ergodicSMul_iterateMulAct — Mathlib

English

Ergodicity of the action by an iterate of a measurable map f is equivalent to ergodicity of f itself, under suitable hypotheses.

Русский

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

LaTeX

$$$\text{ergodicSMul}\ (IterateMulAct\ f)\ X\ μ \iff Ergodic f μ$$$

Lean4

theorem ergodicSMul_iterateMulAct {f : α → α} (hf : Measurable f) : ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ :=
  by
  simp only [ergodicSMul_iff, smulInvariantMeasure_iterateMulAct, hf]
  refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩
  · intro s hm hs
    refine h₂ hm fun n ↦ ?_
    nth_rewrite 2 [← Function.IsFixedPt.preimage_iterate hs n.val]
    rfl
  · intro s hm hs
    exact h.quasiErgodic.aeconst_set₀ hm.nullMeasurableSet <| hs (.mk 1)

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