Ergodicity of an irrational rotation #
In this file we prove that rotation of AddCircle p by a is ergodic
if and only if a has infinite order (in other words, if a / p is irrational).
theorem
AddCircle.ergodic_add_left
{p : ℝ}
[Fact (0 < p)]
{a : AddCircle p}
:
Ergodic (fun (x : AddCircle p) => a + x) MeasureTheory.volume ↔ addOrderOf a = 0
theorem
AddCircle.ergodic_add_right
{p : ℝ}
[Fact (0 < p)]
{a : AddCircle p}
:
Ergodic (fun (x : AddCircle p) => x + a) MeasureTheory.volume ↔ addOrderOf a = 0