Documentation

Mathlib.Dynamics.Ergodic.AddCircleAdd

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} :