ergodic_add_right — Mathlib

English

For a ∈ AddCircle(p), the right translation by a, y ↦ y + a, is ergodic on AddCircle(p) with respect to the natural Haar measure if and only if a has infinite additive order (addOrderOf a = 0).

Русский

Пусть a ∈ AddCircle(p). Правый сдвиг y ↦ y + a эргодичен на AddCircle(p) по мере Хаара тогда и только тогда, когда a имеет бесконечный порядковый член (addOrderOf a = 0).

LaTeX

$$$\mathrm{Ergodic}(y\mapsto y+a)\ (\text{на } \mathrm{AddCircle}(p).\text{volume})\iff \mathrm{addOrderOf}(a)=0.$$$

Lean4

theorem ergodic_add_right {a : AddCircle p} : Ergodic (· + a) ↔ addOrderOf a = 0 := by
  simp only [add_comm, ← ergodic_add_left]

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