Commit 2025-04-02 18:47 ccb2aeb2

View on Github →

feat(Ergodic): Radon-Nikodym derivatives of invariant measures (#23462)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

added theorem MeasureTheory.MeasurePreserving.measure_preimage_le

added theorem MeasureTheory.MeasurePreserving.preimage_null

Created Mathlib/Dynamics/Ergodic/RadonNikodym.lean

added theorem MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem MeasureTheory.Measure.MutuallySingular.haveLebesgueDecomposition

deleted theorem MeasureTheory.Measure.MutuallySingular.singularPart

added theorem MeasureTheory.Measure.singularPart_eq_restrict'

added theorem MeasureTheory.Measure.singularPart_eq_restrict

modified theorem MeasureTheory.Measure.singularPart_eq_self