Radon-Nikodym derivative of invariant measures

Given two finite invariant measures of a self-map, we prove that their singular parts, their absolutely continuous parts, and their Radon-Nikodym derivatives are invariant too.

For the first two theorems, we only assume that one of the measures is finite and the other is σ-finite.

TODO

It isn't clear if the finiteness assumptions are optimal in this file. We should either weaken them, or describe an example showing that it's impossible.

theorem MeasureTheory.MeasurePreserving.singularPart {X : Type u_1} {m : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [SigmaFinite ν] {f : X → X} (hfμ : MeasurePreserving f μ μ) (hfν : MeasurePreserving f ν ν) : MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)

The singular part of a finite invariant measure of a self-map with respect to a σ-finite invariant measure is an invariant measure.

theorem MeasureTheory.MeasurePreserving.withDensity_rnDeriv {X : Type u_1} {m : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [SigmaFinite ν] {f : X → X} (hfμ : MeasurePreserving f μ μ) (hfν : MeasurePreserving f ν ν) : MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))

The absolutely continuous part of a finite invariant measure of a self-map with respect to a σ-finite invariant measure is an invariant measure.

theorem MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq {X : Type u_1} {m : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {f : X → X} (hfμ : MeasurePreserving f μ μ) (hfν : MeasurePreserving f ν ν) : μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

The Radon-Nikodym derivative of a finite invariant measure of a self-map f with respect to another finite invariant measure of f is a.e. invariant under f.