Commit 2023-06-10 03:42 e19bd9e9

View on Github →

feat: port MeasureTheory.Measure.Portmanteau (#4938)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Portmanteau.lean

added theorem MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto

added theorem MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto

added theorem MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto

added theorem MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'

added theorem MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto

added theorem MeasureTheory.exists_null_frontier_thickening

added theorem MeasureTheory.exists_null_frontiers_thickening

added theorem MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le

added theorem MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le

added theorem MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge

added theorem MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure

added theorem MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl

added theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator

added theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator

added theorem MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed

added theorem MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le

added theorem MeasureTheory.tendsto_measure_of_null_frontier