Commit 2024-03-21 12:35 51ab0bbf

View on Github →

chore(MeasureTheory.Decomposition.Lebesgue): cleaning and a few new basic lemmas (#11561) Move lemmas to put similar ones together, replace refine' by refine and => by ↦. Lemmas added:

singularPart_add_rnDeriv and rnDeriv_add_singularPart: almost aliases of haveLebesgueDecomposition_add
haveLebesgueDecomposition_smul', haveLebesgueDecomposition_rnDeriv
singularPart_eq_zero_of_ac, singularPart_eq_zero, singularPart_self, singularPart_eq_self

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

modified theorem MeasureTheory.Measure.MutuallySingular.rnDeriv_ae_eq_zero

modified theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv

modified theorem MeasureTheory.Measure.eq_rnDeriv₀

modified theorem MeasureTheory.Measure.eq_withDensity_rnDeriv₀

modified theorem MeasureTheory.Measure.integrable_toReal_rnDeriv

modified theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top

added theorem MeasureTheory.Measure.rnDeriv_add_singularPart

modified theorem MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition

modified theorem MeasureTheory.Measure.rnDeriv_self

added theorem MeasureTheory.Measure.singularPart_add_rnDeriv

added theorem MeasureTheory.Measure.singularPart_eq_self

added theorem MeasureTheory.Measure.singularPart_eq_zero

added theorem MeasureTheory.Measure.singularPart_eq_zero_of_ac

modified theorem MeasureTheory.Measure.singularPart_of_not_haveLebesgueDecomposition

added theorem MeasureTheory.Measure.singularPart_self

modified theorem MeasureTheory.Measure.singularPart_withDensity

modified theorem MeasureTheory.Measure.singularPart_zero