Commit 2024-07-12 22:59 de620253

View on Github →

feat(Decomposition/Lebesgue): SigmaFinite -> SFinite (#14658) Also generalize exists_absolutelyContinuous_isFiniteMeasure and some downstream lemmas. Deletions:

MeasureTheory.Measure.restrict.instIsFiniteMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

modified theorem Besicovitch.exists_closedBall_covering_tsum_measure_le

modified theorem Besicovitch.exists_disjoint_closedBall_covering_ae

modified theorem Besicovitch.exists_disjoint_closedBall_covering_ae_aux

modified theorem Besicovitch.tendsto_filterAt

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem MeasureTheory.Measure.HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

modified theorem MeasureTheory.Measure.rnDeriv_pos'

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

modified theorem volume_regionBetween_eq_lintegral

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

modified theorem MeasureTheory.exists_null_frontier_thickening

modified theorem MeasureTheory.exists_null_frontiers_thickening

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

modified theorem MeasureTheory.sum_restrict_disjointed_spanningSets

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

deleted theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

modified theorem MeasureTheory.withDensity_tsum