English
The absolutely continuous part of a finite invariant measure of a self-map with respect to a σ-finite invariant measure is invariant under the map.
Русский
Абсолютно непрерывная часть конечной инвариантной меры по отношению к σ-сконечной инвариантной мере инвариантна относительно той же карты.
LaTeX
$$$\text{MeasurePreserving } f \; μ \; μ \rightarrow \text{MeasurePreserving } f \; (ν.\text{withDensity}(μ.rnDeriv ν)) (ν.\text{withDensity}(μ.rnDeriv ν))$$$
Lean4
/-- The absolutely continuous part of a finite invariant measure of a self-map
with respect to a σ-finite invariant measure is an invariant measure. -/
protected theorem withDensity_rnDeriv [SigmaFinite ν] {f : X → X} (hfμ : MeasurePreserving f μ μ)
(hfν : MeasurePreserving f ν ν) : MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν)) :=
by
use hfμ.measurable
ext s hs
rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs, ← add_apply,
rnDeriv_add_singularPart, ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
