English
The Haar (quotient) measure on AddCircle T arises from Lebesgue measure on ℝ restricted to a period interval; more precisely, the quotient measure on AddCircle T equals the preimage measure from volume restricted to a representative interval, i.e. the induced measure from the fundamental domain.
Русский
Гаарова (факторная) мера на AddCircle T получается из линейной меры на ℝ, ограниченной на периодический интервал; точнее, мера фактор-гомоморфизма AddCircle T равна мере-предобразованию от объёма, ограниченного на образецный интервал.
LaTeX
$$$\\text{AddCircle measure is the quotient preimage of volume on a fundamental domain: }\\mathrm{vol}(U)=\\mathrm{vol}(\\{x\\in\\mathrm{Ioc}(t,t+T): \\tilde{x}\\in U\\})$$$
Lean4
instance : AddQuotientMeasureEqMeasurePreimage volume (volume : Measure (AddCircle T)) :=
by
apply MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage
simp [(isAddFundamentalDomain_Ioc' hT.out 0).covolume_eq_volume, AddCircle.measure_univ]
