English
An alternate formulation of the half-interval case, relating curveIntegralFun on the concatenated path to the scaled curveIntegralFun on the second segment.
Русский
Альтернативная формулировка случая через середину: связывает curveIntegralFun по объединённому пути с масштабированным curveIntegralFun по второй части.
LaTeX
$$$ \\operatorname{curveIntegralFun}(\\omega, γ_{ab}.trans γ_{bc}, t) = 2 \\cdot \\operatorname{curveIntegralFun}(\\omega, γ_{bc}, 2t-1) $ for suitable t$$
Lean4
theorem curveIntegralFun_trans_aeeq_left (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) :
curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ι (0 : ℝ) (1 / 2))] fun t ↦
(2 : ℕ) • curveIntegralFun ω γab (2 * t) :=
by
rw [uIoc_of_le (by positivity), ← restrict_Ioo_eq_restrict_Ioc]
filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₀, ht⟩
exact curveIntegralFun_trans_of_lt_half ω γab γbc ht
