Commit 2024-10-11 13:11 69715a18

View on Github →

feat(Measure/WithDensityFinite): redefine Measure.toFinite (#17421)

Redefine Measure.toFinite using exists_isFiniteMeasure_absolutelyContinuous.
Redefine Measure.densityToFinite as rnDeriv, deprecate it.
Drop some lemmas about toFiniteAux.
Simplify proofs.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.sFiniteSeq_le

modified theorem MeasureTheory.sFiniteSeq_zero

Modified Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

deleted def MeasureTheory.Measure.densityToFinite

modified theorem MeasureTheory.absolutelyContinuous_toFinite

added theorem MeasureTheory.ae_toFinite

added theorem MeasureTheory.ae_toFiniteAux

added theorem MeasureTheory.isFiniteMeasure_toFiniteAux

deleted theorem MeasureTheory.sFiniteSeq_absolutelyContinuous_toFiniteAux

deleted theorem MeasureTheory.toFiniteAux_absolutelyContinuous_toFinite

deleted theorem MeasureTheory.toFiniteAux_apply

deleted theorem MeasureTheory.toFiniteAux_eq_zero_iff

deleted theorem MeasureTheory.toFiniteAux_univ_le_one

deleted theorem MeasureTheory.toFiniteAux_zero

modified theorem MeasureTheory.toFinite_absolutelyContinuous

deleted theorem MeasureTheory.toFinite_apply

added theorem MeasureTheory.toFinite_apply_eq_zero_iff

added theorem MeasureTheory.toFinite_eq_self

modified theorem MeasureTheory.toFinite_zero