English
Let f be ergodic and g be a.e. strongly measurable; if g is invariant a.e., then g is a.e. constant.
Русский
Пусть f эргодичен, g — почти surely сильно измеримая; если g инвариантна по отношению к f почти всюду, то g константа почти всюду.
LaTeX
$$$[Ergodic(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 an ergodic map.
Let `g : α → X` be a null-measurable function from `α` to a nonempty measurable space
with a countable family of measurable sets separating the points of `X`.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant. -/
theorem ae_eq_const_of_ae_eq_comp₀ (h : Ergodic f μ) (hgm : NullMeasurable g μ) (hg_eq : g ∘ f =ᵐ[μ] g) :
∃ c, g =ᵐ[μ] const α c :=
h.quasiErgodic.ae_eq_const_of_ae_eq_comp₀ hgm hg_eq
