English
If a measure-preserving equivalence e maps μ to μ', then ergodicity of e ∘ f ∘ e^{-1} with respect to μ' is equivalent to ergodicity of f with respect to μ.
Русский
Если эквивалентность e сохраняет меру и переводит μ в μ', то эргодичность e ∘ f ∘ e^{-1} относительно μ' эквивалентна эргодичности f относительно μ.
LaTeX
$$$\mathrm{Ergodic}(e\circ f\circ e^{-1}, \mu') \iff \mathrm{Ergodic}(f, \mu)$$$
Lean4
theorem ergodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') : Ergodic (e ∘ f ∘ e.symm) μ' ↔ Ergodic f μ :=
by
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
exact
⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with }, fun hf =>
{ this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩
