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 equalAddCircle.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}
{ε : ℝ}
:
Metric.closedBall x ε =ᵐ[MeasureTheory.volume] Metric.ball x ε
theorem
AddCircle.isAddFundamentalDomain_of_ae_ball
{T : ℝ}
[hT : Fact (0 < T)]
(I : Set (AddCircle T))
(u x : AddCircle T)
(hu : IsOfFinAddOrder u)
(hI : 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.
theorem
AddCircle.volume_of_add_preimage_eq
{T : ℝ}
[hT : Fact (0 < T)]
(s I : Set (AddCircle T))
(u x : AddCircle T)
(hu : IsOfFinAddOrder u)
(hs : u +ᵥ s =ᵐ[MeasureTheory.volume] s)
(hI : I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u))))
:
MeasureTheory.volume s = addOrderOf u • MeasureTheory.volume (s ∩ I)