English
The projection from the real line to UnitAddCircle (T = 1) is measure-preserving with respect to the restricted Lebesgue measure on Ioc t (t+1) and the Haar measure on UnitAddCircle.
Русский
Проекция из ℝ на UnitAddCircle с периодом 1 сохраняет меру между ограниченной мерой Лебега на Ioc(t,t+1) и мерами на UnitAddCircle.
LaTeX
$$$\\text{measurePreserving mk}_{t}^{(1)}: (\\mathrm{volume}\\restriction \\mathrm{Ioc}(t,t+1)) \\to \\mathrm{volume}_{UnitAddCircle}$$$
Lean4
/-- The covering map from `ℝ` to the "unit additive circle" `ℝ ⧸ ℤ` is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass 1)
on the additive circle, and with respect to the restriction of Lebesgue measure on `ℝ` to an
interval (t, t + 1]. -/
protected theorem measurePreserving_mk (t : ℝ) :
MeasurePreserving (β := UnitAddCircle) ((↑) : ℝ → UnitAddCircle) (volume.restrict (Ioc t (t + 1))) :=
AddCircle.measurePreserving_mk 1 t
