English
For a quasi-ergodic map, if a set s is null-measurable and essentially invariant (up to ae equality) under f, then the set is almost surely constant with respect to ae μ.
Русский
Для квазиерегодной карты, если множество s нуль-измеримо и практически инвариантно относительно f, то множество почти surely константно по отношению к ae μ.
LaTeX
$$$\mathrm{aeconst\_set}\ (hf, hsm, hs) : \mathrm{EventuallyConst}(s, \mathrm{ae}\,\mu)$$$
Lean4
theorem aeconst_set₀ (hf : QuasiErgodic f μ) (hsm : NullMeasurableSet s μ) (hs : f ⁻¹' s =ᵐ[μ] s) :
EventuallyConst s (ae μ) :=
let ⟨_t, h₀, h₁, h₂⟩ := hf.toQuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae hsm hs
(hf.aeconst_set h₀ h₂).congr h₁
