preErgodic_of_preErgodic_conjugate

English

If a measure-preserving map g from (α, μ) to (β, μ') intertwines f with f' (i.e., g is a conjugacy in the semiconjugacy sense), and f is PreErgodic with respect to μ, then f' is PreErgodic with respect to μ'.

Русский

Пусть g: α → β сохраняет меру и связывает f и f' (полу сопряжение). Тогда если f предергодичен относительно μ, то f' предергодичен относительно μ'.

LaTeX

$$$\mathrm{MeasurePreserving}(g, \mu, \mu') \land \mathrm{PreErgodic}(f, \mu) \land \mathrm{Semiconj}(g, f, f') \Rightarrow \mathrm{PreErgodic}(f', \mu')$$$

Lean4

theorem preErgodic_of_preErgodic_conjugate (hg : MeasurePreserving g μ μ') (hf : PreErgodic f μ) {f' : β → β}
    (h_comm : Semiconj g f f') : PreErgodic f' μ' where
  aeconst_set s hs₀
    hs₁ := by
    rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]
    apply hf.aeconst_set (hg.measurable hs₀)
    rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]

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