English
Let f be quasi-ergodic and g: α → X be null-measurable with X countably separated. If g is a.e.-invariant under f, then g is a.e. constant.
Русский
Пусть f — квазир ergodic, а g: α → X — нулево- измеримая функция в пространство X, разделяемое счётной семейством множеств. Если g инвариантна по отношению к f почти всюду, то g почти всюду константа.
LaTeX
$$$[QuasiErgodic(f, \\\\mu)] \\\\wedge [NullMeasurable(g, \\\\mu)] \\\\wedge (g \\\\circ f =\\\\, g) \\\\Rightarrow \\\\exists c: X, g = \\\\text{a.e. const}(\\\\alpha, c)$$$
Lean4
/-- Let `f : α → α` be a (quasi)ergodic map. Let `g : α → X` is a null-measurable function
from `α` to a nonempty space with a countable family of measurable sets
separating points of a set `s` such that `f x ∈ s` for a.e. `x`.
If `g` that is a.e.-invariant under `f`, then `g` is a.e. constant. -/
theorem ae_eq_const_of_ae_eq_comp_of_ae_range₀ [Nonempty X] [MeasurableSpace X] {s : Set X}
[MeasurableSpace.CountablySeparated s] {f : α → α} {g : α → X} (h : QuasiErgodic f μ) (hs : ∀ᵐ x ∂μ, g x ∈ s)
(hgm : NullMeasurable g μ) (hg_eq : g ∘ f =ᵐ[μ] g) : ∃ c, g =ᵐ[μ] const α c :=
by
refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_
refine fun U hU ↦ h.ae_mem_or_ae_notMem₀ (s := g ⁻¹' U) (hgm hU) ?_b
refine (hg_eq.mono fun x hx ↦ ?_).set_eq
rw [← preimage_comp, mem_preimage, mem_preimage, hx]
