Commit 2023-11-12 18:17 daf40d2c

View on Github →

feat(MeasureTheory): remove an AbsolutelyContinuous hypothesis from inv_rnDeriv (#8351) In order to remove that hypothesis, we also:

add some basic lemmas about absolute continuity and mutually singular measures.
add HaveLebesgueDecomposition instances
rewrite the proof of withDensity_rnDeriv_eq to use the new API instead of unfolding the definitions
generalize rnDeriv_restrict and rnDeriv_withDensity to possibly different measures

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem AEMeasurable.singularPart

added theorem AEMeasurable.withDensity_rnDeriv

added theorem MeasureTheory.Measure.MutuallySingular.singularPart

added theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv

added theorem MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular

deleted theorem MeasureTheory.Measure.rnDeriv_restrict

added theorem MeasureTheory.Measure.rnDeriv_restrict_self

added theorem MeasureTheory.Measure.rnDeriv_self

added theorem MeasureTheory.Measure.rnDeriv_singularPart

added theorem MeasureTheory.Measure.rnDeriv_zero

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.inv_rnDeriv'

modified theorem MeasureTheory.Measure.inv_rnDeriv

added theorem MeasureTheory.Measure.inv_rnDeriv_aux

added theorem MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular

added theorem MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular'

added theorem MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular

added theorem MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular

added theorem MeasureTheory.Measure.rnDeriv_pos'

added theorem MeasureTheory.Measure.rnDeriv_restrict

added theorem MeasureTheory.Measure.rnDeriv_withDensity_left

added theorem MeasureTheory.Measure.rnDeriv_withDensity_left_of_absolutelyContinuous

added theorem MeasureTheory.Measure.rnDeriv_withDensity_right

added theorem MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous

added theorem MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv

added theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left

added theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.AbsolutelyContinuous.add_right

added theorem MeasureTheory.Measure.AbsolutelyContinuous.restrict

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

added theorem MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet

added theorem MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet

added theorem MeasureTheory.Measure.MutuallySingular.measure_nullSet

added def MeasureTheory.Measure.MutuallySingular.nullSet

added theorem MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet

added theorem MeasureTheory.Measure.MutuallySingular.restrict_nullSet

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.Measure.MutuallySingular.withDensity