ergodic_add_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ergodic_add_left {a : AddCircle p} : Ergodic (a + ·) ↔ addOrderOf a = 0 := by
  rw [← denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul]

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