# Documentation

The file is a place to collect measure-theoretic results about the additive circle.

## Main definitions: #

• AddCircle.closedBall_ae_eq_ball: open and closed balls in the additive circle are almost equal
• AddCircle.isAddFundamentalDomain_of_ae_ball: a ball is a fundamental domain for rational angle rotation in the additive circle
theorem AddCircle.closedBall_ae_eq_ball {T : } [hT : Fact (0 < T)] {x : } {ε : } :
=ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume]
theorem AddCircle.isAddFundamentalDomain_of_ae_ball {T : } [hT : Fact (0 < T)] (I : Set ()) (u : ) (x : ) (hu : ) (hI : I =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] Metric.ball x (T / (2 * ↑()))) :

Let G be the subgroup of AddCircle T generated by a point u of finite order n : ℕ. Then any set I that is almost equal to a ball of radius T / 2n is a fundamental domain for the action of G on AddCircle T by left addition.

theorem AddCircle.volume_of_add_preimage_eq {T : } [hT : Fact (0 < T)] (s : Set ()) (I : Set ()) (u : ) (x : ) (hu : ) (hs : u +ᵥ s =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] s) (hI : I =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] Metric.ball x (T / (2 * ↑()))) :
MeasureTheory.volume s = MeasureTheory.volume (s I)