Ergodic maps of the additive circle

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

Main definitions:

• AddCircle.ergodic_zsmul: given n : ℤ such that 1 < |n|, the self map y ↦ n • y on the additive circle is ergodic (wrt the Haar measure).
• AddCircle.ergodic_nsmul: given n : ℕ such that 1 < n, the self map y ↦ n • y on the additive circle is ergodic (wrt the Haar measure).
• AddCircle.ergodic_zsmul_add: given n : ℤ such that 1 < |n| and x : AddCircle T, the self map y ↦ n • y + x on the additive circle is ergodic (wrt the Haar measure).
• AddCircle.ergodic_nsmul_add: given n : ℕ such that 1 < n and x : AddCircle T, the self map y ↦ n • y + x on the additive circle is ergodic (wrt the Haar measure).

theorem AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self {T : ℝ} [hT : Fact (0 < T)] {s : Set (AddCircle T)} (hs : MeasureTheory.NullMeasurableSet s) {ι : Type u_1} {l : Filter ι} [Filter.NeBot l] {u : ι → AddCircle T} (hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] s) (hu₂ : Filter.Tendsto (addOrderOf ∘ u) l Filter.atTop) : s =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] Set.univ

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 AddCircle.ergodic_zsmul {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} (hn : 1 < |n|) : Ergodic fun (y : AddCircle T) => n • y

theorem AddCircle.ergodic_nsmul {T : ℝ} [hT : Fact (0 < T)] {n : ℕ} (hn : 1 < n) : Ergodic fun (y : AddCircle T) => n • y

theorem AddCircle.ergodic_zsmul_add {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℤ} (h : 1 < |n|) : Ergodic fun (y : AddCircle T) => n • y + x

theorem AddCircle.ergodic_nsmul_add {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℕ} (h : 1 < n) : Ergodic fun (y : AddCircle T) => n • y + x