English
Let f be a (pre)ergodic map. If g is measurable and invariant under f, then g is a.e. constant.
Русский
Пусть f — предэргодический отображатель. Если g измерима и инвариантна относительно f, то g константа почти всюду.
LaTeX
$$$[PreErgodic(f, \\\\mu)] \\\\wedge [Measurable(g)] \\\\wedge (g \\\\circ f = g) \\\\Rightarrow \\\\exists c, g = \\\\text{a.e. const}(\\\\alpha, c)$$$
Lean4
/-- Let `f : α → α` be a (pre)ergodic map.
Let `g : α → X` be a measurable function from `α` to a nonempty measurable space
with a countable family of measurable sets separating the points of `X`.
If `g` is invariant under `f`, then `g` is a.e. constant. -/
theorem ae_eq_const_of_ae_eq_comp (h : PreErgodic f μ) (hgm : Measurable g) (hg_eq : g ∘ f = g) :
∃ c, g =ᵐ[μ] const α c :=
exists_eventuallyEq_const_of_forall_separating MeasurableSet fun U hU ↦
h.ae_mem_or_ae_notMem (s := g ⁻¹' U) (hgm hU) <| by rw [← preimage_comp, hg_eq]
