eq_const_of_compQuasiMeasurePreserving_eq

English

Let f be quasi-ergodic and g: α → X be a.e.-strongly measurable. If g ∘ f =ᵐ g, then ∃ c with g =ᵐ const α c.

Русский

Пусть f квазир эргодичен, g:a.e.-сильно измерима. Если g ∘ f =ᵐ g, то ∃ c: X, g =ᵐ const α c.

LaTeX

$$∃ c, (g =ᵐ[μ] const α c)$$

Lean4

theorem eq_const_of_compQuasiMeasurePreserving_eq (h : QuasiErgodic f μ) {g : α →ₘ[μ] X}
    (hg_eq : g.compQuasiMeasurePreserving f h.1 = g) : ∃ c, g = .const α c :=
  have : g ∘ f =ᵐ[μ] g := (g.coeFn_compQuasiMeasurePreserving h.1).symm.trans (hg_eq.symm ▸ .refl _ _)
  let ⟨c, hc⟩ := h.ae_eq_const_of_ae_eq_comp_ae g.aestronglyMeasurable this
  ⟨c, AEEqFun.ext <| hc.trans (AEEqFun.coeFn_const _ _).symm⟩

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