Theorems · Theorem · measure theory

AddCircle.isAddFundamentalDomain_of_ae_ball

∀ {T : ℝ} [hT : Fact (0 < T)] (I : Set (AddCircle T)) (u x : AddCircle T),
  IsOfFinAddOrder u →
    I =ᵐ[MeasureTheory.volume] 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.

Defined in

Mathlib.MeasureTheory.Group.AddCircle

Cited by

1 results in Mathlib

Foundations

Depth 250 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact