English
The Radon–Nikodym derivative μ.rnDeriv ν is almost everywhere invariant under f when f preserves μ and ν.
Русский
Радиан-никодийная производная μ.rnDeriv ν почти всюду инвариантна относительно f при сохранении μ и ν.
LaTeX
$$$\\mu\\text{.rnDeriv } ν \\circ f =^{a.e.}_{ν} \\mu\\text{.rnDeriv } ν$$$
Lean4
/-- 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`. -/
theorem rnDeriv_comp_aeEq [IsFiniteMeasure ν] {f : X → X} (hfμ : MeasurePreserving f μ μ)
(hfν : MeasurePreserving f ν ν) : μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν :=
by
wlog hμν : μ ≪ ν generalizing μ
· specialize this (hfμ.withDensity_rnDeriv hfν) (withDensity_absolutelyContinuous _ _)
refine .trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))
apply hfν.quasiMeasurePreserving.ae_eq_comp
exact (rnDeriv_withDensity ν (measurable_rnDeriv μ ν)).symm
refine .of_forall_eventually_lt_iff fun c ↦ ?_
set s := {a | μ.rnDeriv ν a < c}
have hsm : MeasurableSet s := measurable_rnDeriv _ _ measurableSet_Iio
have hμ_diff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s) :=
measure_diff_symm (hfμ.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
(hfμ.measure_preimage hsm.nullMeasurableSet) (measure_ne_top _ _)
have hν_diff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s) :=
measure_diff_symm (hfν.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
(hfν.measure_preimage hsm.nullMeasurableSet) (measure_ne_top _ _)
suffices f ⁻¹' s =ᵐ[ν] s from this.mem_iff
suffices ν (f ⁻¹' s \ s) = 0 from (ae_le_set.mpr this).antisymm (ae_le_set.mpr <| hν_diff ▸ this)
contrapose! hμ_diff with h₀
apply ne_of_gt
calc
μ (s \ f ⁻¹' s) = ∫⁻ a in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν := (setLIntegral_rnDeriv hμν _).symm
_ < ∫⁻ _ in s \ f ⁻¹' s, c ∂ν :=
by
apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
· rw [setLIntegral_rnDeriv hμν]
apply measure_ne_top
· exact .of_forall fun x hx ↦ hx.1
_ = ∫⁻ _ in f ⁻¹' s \ s, c ∂ν := by simp [hν_diff]
_ ≤ ∫⁻ a in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν := (setLIntegral_mono (by fun_prop) (fun x hx ↦ not_lt.mp hx.2))
_ = μ (f ⁻¹' s \ s) := setLIntegral_rnDeriv hμν _
