English
The covering map from ℝ to AddCircle T is measure-preserving when the domain carries the Lebesgue measure restricted to a length-T interval and the codomain carries the Haar measure on the additive circle.
Русский
Покрывающая карта из ℝ в AddCircle T сохраняет меру, когда область на стороне источника имеет ограниченную длину-T и кодомона — гааровская мера на кольце прибавления.
LaTeX
$$$\\text{Quotient map }\\operatorname{mk}: \\mathbb{R} \\to \\mathrm{AddCircle}(T)\\; \\text{is measure-preserving for }(\\mathrm{volume}\\restriction \\mathrm{Ioc}(t,t+T),\\; \\mathrm{volume}_{\\mathrm{AddCircle}(T)})$$$
Lean4
/-- The covering map from `ℝ` to the "additive circle" `ℝ ⧸ (ℤ ∙ T)` is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass `T`)
on the additive circle, and with respect to the restriction of Lebesgue measure on `ℝ` to an
interval (t, t + T]. -/
protected theorem measurePreserving_mk (t : ℝ) :
MeasurePreserving (β := AddCircle T) ((↑) : ℝ → AddCircle T) (volume.restrict (Ioc t (t + T))) :=
measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage volume (𝓕 := Ioc t (t + T))
(isAddFundamentalDomain_Ioc' hT.out _) _
