Commit 2024-04-08 12:14 b8fc37d6

View on Github →

feat(MeasureTheory): add singularPart and rnDeriv lemmas (#11883) Also golf and move rnDeriv_restrict.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem MeasureTheory.Measure.rnDeriv_restrict

added theorem MeasureTheory.Measure.singularPart_restrict

added theorem MeasureTheory.Measure.singularPart_singularPart

added theorem MeasureTheory.Measure.singularPart_zero_right

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

deleted theorem MeasureTheory.Measure.rnDeriv_restrict

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

added theorem MeasureTheory.Measure.MutuallySingular.restrict

Modified Mathlib/MeasureTheory/Measure/Trim.lean

added theorem MeasureTheory.Measure.AbsolutelyContinuous.trim

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.trim_withDensity