# mathlib3documentation

dynamics.ergodic.add_circle

# Ergodic maps of the additive circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains proofs of ergodicity for maps of the additive circle.

## Main definitions: #

• add_circle.ergodic_zsmul: given n : ℤ such that 1 < |n|, the self map y ↦ n • y on the additive circle is ergodic (wrt the Haar measure).
• add_circle.ergodic_nsmul: given n : ℕ such that 1 < n, the self map y ↦ n • y on the additive circle is ergodic (wrt the Haar measure).
• add_circle.ergodic_zsmul_add: given n : ℤ such that 1 < |n| and x : add_circle T, the self map y ↦ n • y + x on the additive circle is ergodic (wrt the Haar measure).
• add_circle.ergodic_nsmul_add: given n : ℕ such that 1 < n and x : add_circle T, the self map y ↦ n • y + x on the additive circle is ergodic (wrt the Haar measure).
theorem add_circle.ae_empty_or_univ_of_forall_vadd_ae_eq_self {T : } [hT : fact (0 < T)] {s : set (add_circle T)} {ι : Type u_1} {l : filter ι} [l.ne_bot] {u : ι } (hu₁ : (i : ι), ) (hu₂ : l filter.at_top) :

If a null-measurable subset of the circle is almost invariant under rotation by a family of rational angles with denominators tending to infinity, then it must be almost empty or almost full.

theorem add_circle.ergodic_zsmul {T : } [hT : fact (0 < T)] {n : } (hn : 1 < |n|) :
theorem add_circle.ergodic_nsmul {T : } [hT : fact (0 < T)] {n : } (hn : 1 < n) :
theorem add_circle.ergodic_zsmul_add {T : } [hT : fact (0 < T)] (x : add_circle T) {n : } (h : 1 < |n|) :
theorem add_circle.ergodic_nsmul_add {T : } [hT : fact (0 < T)] (x : add_circle T) {n : } (h : 1 < n) :