ergodic_nsmul_add — Mathlib

English

Let T > 0 and x ∈ AddCircle(T). For every n ∈ ℕ with n > 1, the affine map f(y) = n · y + x on AddCircle(T) is ergodic with respect to the natural Haar (volume) measure on AddCircle(T).

Русский

Пусть T > 0 и x ∈ AddCircle(T). Для любого n ∈ ℕ с n > 1 аффинное отображение f(y) = n · y + x на AddCircle(T) эргодично относительно естественной меры Хаара (объём на AddCircle(T)).

LaTeX

$$$\forall T>0\,\forall x\in \mathrm{AddCircle}(T)\,\forall n\in\mathbb{N},\ 1

Lean4

theorem ergodic_nsmul_add (x : AddCircle T) {n : ℕ} (h : 1 < n) : Ergodic fun y => n • y + x :=
  ergodic_zsmul_add x (by simp [h] : 1 < |(n : ℤ)|)

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