English
If ν is absolutely continuous w.r.t. μ and f preserves ν, then ν equals c • μ for some c ≠ 0,1 depending on normalization.
Русский
Если ν абсолютно непрерывна относительно μ и f сохраняет ν, тогда ν = c • μ для некоторого c.
LaTeX
$$$\exists c : \mathbb{R}_{\ge 0}^{\infty}, \; \nu = c \cdot \mu$$$
Lean4
theorem eq_smul_of_absolutelyContinuous [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ : Ergodic f μ)
(hfν : MeasurePreserving f ν ν) (hνμ : ν ≪ μ) : ∃ c : ℝ≥0∞, ν = c • μ :=
by
have := hfν.rnDeriv_comp_aeEq hμ.toMeasurePreserving
obtain ⟨c, hc⟩ := hμ.ae_eq_const_of_ae_eq_comp₀ (measurable_rnDeriv _ _).nullMeasurable this
use c
ext s hs
calc
ν s = ∫⁻ a in s, ν.rnDeriv μ a ∂μ := .symm <| setLIntegral_rnDeriv hνμ _
_ = ∫⁻ _ in s, c ∂μ := (lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self)
_ = (c • μ) s := by simp
