AddCircle.isAddFundamentalDomain_of_ae_ball

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

This theorem, named `AddCircle.isAddFundamentalDomain_of_ae_ball`, states the following: given a subgroup `G` of the additive circle `AddCircle T`, which is generated by a point `u` of finite order `n`, and given a set `I` that is almost everywhere equivalent to a ball with radius `T / (2n)`, then `I` serves as a fundamental domain for the action of `G` on `AddCircle T` via left addition. Here, 'almost everywhere equivalent' means that the equivalence holds except on a set of measure zero. The finite order `n` of the point `u` is denoted by `addOrderOf u`. The ball with center at `x` and radius `T / (2n)` is denoted by `Metric.ball x (T / (2 * ↑(addOrderOf u)))`.

More concisely: Given a subgroup of the additive circle generated by a point of finite order and a set almost everywhere equivalent to a ball with radius T/(2n), this ball serves as a fundamental domain for the action of the subgroup via left addition.