preErgodic_conjugate_iff — Mathlib

English

For a measure-preserving equivalence e between spaces, PreErgodicity of the conjugated system is equivalent to PreErgodicity of the original system.

Русский

Для меро-сохраняющего эквивалентного отображения e между пространствами предергодичность сконъюгированного процесса эквивалентна предэргодичности исходной системы.

LaTeX

$$$\mathrm{PreErgodic}\ (e \circ f \circ e^{-1}, \mu') \;\Leftrightarrow\; \mathrm{PreErgodic}(f, \mu)$$$

Lean4

theorem preErgodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :
    PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ :=
  by
  refine
    ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf ?_, fun hf =>
      preErgodic_of_preErgodic_conjugate h hf ?_⟩
  · simp [Semiconj]
  · simp [Semiconj]

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