Documentation

Mathlib.Dynamics.Ergodic.AddCircle

Ergodic maps of the additive circle #

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

Main definitions: #

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 MeasureTheory.volume) {ι : Type u_1} {l : Filter ι} [l.NeBot] {u : ιAddCircle T} (hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[MeasureTheory.volume] s) (hu₂ : Filter.Tendsto (addOrderOf u) l Filter.atTop) :
s =ᵐ[MeasureTheory.volume] s =ᵐ[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) MeasureTheory.volume
theorem AddCircle.ergodic_nsmul {T : } [hT : Fact (0 < T)] {n : } (hn : 1 < n) :
Ergodic (fun (y : AddCircle T) => n y) MeasureTheory.volume
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) MeasureTheory.volume
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) MeasureTheory.volume