English
The total volume of the whole unit set is 1.
Русский
Общая мера множества равна единице.
LaTeX
$$$\\mathrm{vol}(\\mathrm{Set.univ}) = 1$$$
Lean4
/-- The integral of an almost-everywhere strongly measurable function over `AddCircle T` is equal
to the integral over an interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
protected theorem integral_preimage (t : ℝ) (f : AddCircle T → E) :
(∫ a in Ioc t (t + T), f a) = ∫ b : AddCircle T, f b :=
by
have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
have := integral_map_equiv (μ := volume) (measurableEquivIoc T t).symm f
simp only [measurableEquivIoc, equivIoc, QuotientAddGroup.equivIocMod, MeasurableEquiv.symm_mk,
MeasurableEquiv.coe_mk, Equiv.coe_fn_symm_mk] at this
rw [← (AddCircle.measurePreserving_mk T t).map_eq, ← integral_subtype m, ← this]
have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by ext1 x; rfl
simp_rw [this]
rw [← map_map AddCircle.measurable_mk' measurable_subtype_coe, ← map_comap_subtype_coe m]
rfl
