Measure-theoretic results about the additive circle

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 : AddCircle T} {ε : ℝ} : MeasureTheory.volume.ae.EventuallyEq (Metric.closedBall x ε) (Metric.ball x ε)

theorem AddCircle.isAddFundamentalDomain_of_ae_ball {T : ℝ} [hT : Fact (0 < T)] (I : Set (AddCircle T)) (u : AddCircle T) (x : AddCircle T) (hu : IsOfFinAddOrder u) (hI : MeasureTheory.volume.ae.EventuallyEq I (Metric.ball x (T / (2 * ↑(addOrderOf u))))) : MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I MeasureTheory.volume

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 (AddCircle T)) (I : Set (AddCircle T)) (u : AddCircle T) (x : AddCircle T) (hu : IsOfFinAddOrder u) (hs : MeasureTheory.volume.ae.EventuallyEq (u +ᵥ s) s) (hI : MeasureTheory.volume.ae.EventuallyEq I (Metric.ball x (T / (2 * ↑(addOrderOf u))))) : ↑↑MeasureTheory.volume s = addOrderOf u • ↑↑MeasureTheory.volume (s ∩ I)