English
Let μ and ν be probability measures on the space X and let f: X → X be a map. If f is ergodic with respect to μ, ν is invariant under f (i.e., f preserves ν), and ν is absolutely continuous with respect to μ, then ν = μ.
Русский
Пусть μ и ν — вероятностные меры на множество X, пусть f: X → X. Если f расходится эргодично по μ, ν инвариантна относительно f (то есть f сохраняет ν), и ν абсолютно непрерывна по отношению к μ, тогда ν = μ.
LaTeX
$$$\\\\nu = \\\\mu \\\\quad\\\\text{under\\\\; hypotheses: } \\\\mu, \\\\nu \\\\text{ probabilities } f \\\\text{ ergodic w.r.t. } \\\\mu, \\\\\\n\\\\nu \\\\ll \\\\mu, \\\\text{ and } \\\\nu \\\\text{ is measure-preserving under } f.$$$
Lean4
theorem eq_of_absolutelyContinuous [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hμ : Ergodic f μ)
(hfν : MeasurePreserving f ν ν) (hνμ : ν ≪ μ) : ν = μ :=
eq_of_absolutelyContinuous_measure_univ_eq hμ hfν hνμ <| by simp
