Commit 2023-06-07 07:14 21511d60

View on Github →

feat: port MeasureTheory.Decomposition.RadonNikodym (#4781)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq

added theorem MeasureTheory.Measure.withDensity_rnDeriv_eq

added theorem MeasureTheory.Measure.withDensity_rnDeriv_toReal_eq

added theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq

added theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq