Commit 2024-08-14 03:37 86a406ac

View on Github →

feat (MeasureTheory.Decomposition.RadonNikodym): rnDeriv_le_one_iff_le (#15473) Add rnDeriv_le_one_iff_le and rnDeriv_eq_one_iff_eq.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

modified theorem MeasureTheory.Measure.inv_rnDeriv_aux

added theorem MeasureTheory.Measure.rnDeriv_eq_one_iff_eq

modified theorem MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular

added theorem MeasureTheory.Measure.rnDeriv_le_one_iff_le

modified theorem MeasureTheory.Measure.rnDeriv_pos'

modified theorem MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous