Commit 2024-06-16 18:56 d2d320bc

View on Github →

feat: absolute continuity, Radon-Nikodym derivatives of μ.map f for a measurable embedding f (#13761)

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasurableEmbedding.map_withDensity_rnDeriv

added theorem MeasurableEmbedding.rnDeriv_map

added theorem MeasurableEmbedding.rnDeriv_map_aux

added theorem MeasurableEmbedding.singularPart_map

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasurableEmbedding.absolutelyContinuous_map

modified theorem MeasurableEmbedding.comap_add

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

added theorem MeasurableEmbedding.mutuallySingular_map

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasurableEmbedding.sigmaFinite_map

modified theorem MeasurableEquiv.sigmaFinite_map