add_projection_respects_measure — Mathlib

English

For any measurable subset U of AddCircle T, the measure of U equals the restricted preimage measure of U intersected with the fundamental domain Ioc t (t+T).

Русский

Для любого измеримого множества U в AddCircle T мера U равна мере-предобразованию пересечения U с фундаментальной областью Ioc(t,t+T).

LaTeX

$$$\\mathrm{vol}(U)=\\mathrm{vol}\\bigl((\\operatorname{Quotient.mk})^{-1}(U) \\cap \\mathrm{Ioc}(t,(t+T))\\bigr)$ for measurable $U$$$

Lean4

theorem add_projection_respects_measure (t : ℝ) {U : Set (AddCircle T)} (meas_U : MeasurableSet U) :
    volume U = volume (QuotientAddGroup.mk ⁻¹' U ∩ (Ioc t (t + T))) :=
  (isAddFundamentalDomain_Ioc' hT.out _).addProjection_respects_measure_apply (volume : Measure (AddCircle T)) meas_U

Похожие утверждения