ae_eq_const_of_ae_eq_comp_ae — Mathlib

English

Let f be ergodic and g be AEStronglyMeasurable; if g ∘ f =ᵐ g then ∃ c with g =ᵐ const α c.

Русский

Пусть f эргодичен, g AEStronglyMeasurable; если g ∘ f =ᵐ g, то ∃ c: X, g =ᵐ const α c.

LaTeX

$$$[Ergodic(f, \\\\mu)] \\\\wedge [AEStronglyMeasurable(g, \\\\mu)] \\\\wedge (g \\\\circ f =ᵐ g) \\\\Rightarrow \\\\exists c, g =ᵐ const α c$$$

Lean4

/-- Let `f : α → α` be an 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 : Ergodic f μ) (hgm : AEStronglyMeasurable g μ)
    (hg_eq : g ∘ f =ᵐ[μ] g) : ∃ c, g =ᵐ[μ] const α c :=
  h.quasiErgodic.ae_eq_const_of_ae_eq_comp_ae hgm hg_eq

Похожие утверждения