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: givenn : ℤsuch that1 < |n|, the self mapy ↦ n • yon the additive circle is ergodic (wrt the Haar measure).add_circle.ergodic_nsmul: givenn : ℕsuch that1 < n, the self mapy ↦ n • yon the additive circle is ergodic (wrt the Haar measure).add_circle.ergodic_zsmul_add: givenn : ℤsuch that1 < |n|andx : add_circle T, the self mapy ↦ n • y + xon the additive circle is ergodic (wrt the Haar measure).add_circle.ergodic_nsmul_add: givenn : ℕsuch that1 < nandx : add_circle T, the self mapy ↦ n • y + xon 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)}
(hs : measure_theory.null_measurable_set s measure_theory.measure_space.volume)
{ι : Type u_1}
{l : filter ι}
[l.ne_bot]
{u : ι → add_circle T}
(hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[measure_theory.measure_space.volume] s)
(hu₂ : filter.tendsto (add_order_of ∘ u) 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|) :
ergodic (λ (y : add_circle T), n • y) measure_theory.measure_space.volume
theorem
add_circle.ergodic_nsmul
{T : ℝ}
[hT : fact (0 < T)]
{n : ℕ}
(hn : 1 < n) :
ergodic (λ (y : add_circle T), n • y) measure_theory.measure_space.volume
theorem
add_circle.ergodic_zsmul_add
{T : ℝ}
[hT : fact (0 < T)]
(x : add_circle T)
{n : ℤ}
(h : 1 < |n|) :
ergodic (λ (y : add_circle T), n • y + x) measure_theory.measure_space.volume
theorem
add_circle.ergodic_nsmul_add
{T : ℝ}
[hT : fact (0 < T)]
(x : add_circle T)
{n : ℕ}
(h : 1 < n) :
ergodic (λ (y : add_circle T), n • y + x) measure_theory.measure_space.volume