English
Let f be quasi-ergodic and g be AEStronglyMeasurable; if g ∘ f =ᵐ g then g is a.e. constant.
Русский
Пусть f квазир эргодичен, g AEStronglyMeasurable; если g ∘ f =ᵐ g, то g константа почти всюду.
LaTeX
$$$[QuasiErgodic(f, \\\\mu)] \\\\wedge [AEStronglyMeasurable(g, \\\\mu)] \\\\wedge (g \\\\circ f =ᵐ g) \\\\Rightarrow \\\\exists c, g = \\\\text{a.e. const}(\\\\alpha, c)$$$
Lean4
/-- Let `f : α → α` be a quasi-ergodic map.
Let `g : α → X` be an a.e. strongly measurable function
from `α` to a nonempty metrizable topological space.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant. -/
theorem ae_eq_const_of_ae_eq_comp_ae {g : α → X} (h : QuasiErgodic f μ) (hgm : AEStronglyMeasurable g μ)
(hg_eq : g ∘ f =ᵐ[μ] g) : ∃ c, g =ᵐ[μ] const α c :=
by
borelize X
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩
haveI := ht.secondCountableTopology
exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq
