Commit 2024-09-06 01:46 ed24dd8e

View on Github →

refactor(Measure): move Borel-Cantelli, generalize (#16397)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem MeasureTheory.liminf_ae_eq_of_forall_ae_eq

deleted theorem MeasureTheory.limsup_ae_eq_of_forall_ae_eq

deleted theorem MeasureTheory.measure_liminf_eq_zero

deleted theorem MeasureTheory.measure_limsup_eq_zero

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

deleted theorem MeasureTheory.ae_eventually_not_mem

deleted theorem MeasureTheory.measure_setOf_frequently_eq_zero

Created Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

added theorem MeasureTheory.ae_eventually_not_mem

added theorem MeasureTheory.ae_finite_setOf_mem

added theorem MeasureTheory.liminf_ae_eq_of_forall_ae_eq

added theorem MeasureTheory.limsup_ae_eq_of_forall_ae_eq

added theorem MeasureTheory.measure_liminf_atTop_eq_zero

added theorem MeasureTheory.measure_liminf_cofinite_eq_zero

added theorem MeasureTheory.measure_limsup_atTop_eq_zero

added theorem MeasureTheory.measure_limsup_cofinite_eq_zero

added theorem MeasureTheory.measure_setOf_frequently_eq_zero