English
For any AddCircle T-valued function, the lower integral on Ioc t (t+T) equals the lower integral on AddCircle T of the lifted function.
Русский
Для любой функции AddCircle T-значения интеграл по Ioc(t,t+T) равен интегралу по AddCircle(T) от поднятой функции.
LaTeX
$$$\\int\\!_{a\\in \\mathrm{Ioc}(t,t+T)} f(a)\\,da = \\int\\!_{b\\in \\mathrm{AddCircle}(T)} f(b)\\,db$$$
Lean4
/-- The lower integral of a function over `AddCircle T` is equal to the lower integral over an
interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
protected theorem lintegral_preimage (t : ℝ) (f : AddCircle T → ℝ≥0∞) :
(∫⁻ a in Ioc t (t + T), f a) = ∫⁻ b : AddCircle T, f b :=
by
have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
have := lintegral_map_equiv (μ := volume) f (measurableEquivIoc T t).symm
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]
convert this.symm using 1
· rw [← map_comap_subtype_coe m _]
exact MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _
· congr 1
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
