Commit 2023-08-25 05:30 7f2ee091

View on Github →

feat: Results about convergence of measures of sets assuming convergence of indicator functions. (#6225) Adding results about convergence of measures of sets assuming convergence of indicator functions.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

added theorem measurableSet_of_tendsto_indicator

added theorem nullMeasurableSet_of_tendsto_indicator

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator

added theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure

added theorem MeasureTheory.tendsto_measure_of_tendsto_indicator

added theorem MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

added theorem measurable_indicator_const_iff

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem aemeasurable_indicator_const_iff