English
Let ω be curve-integrable along two successive paths γ_ab and γ_bc. Then the curve integral along their concatenation γ_ab trans γ_bc equals the sum of the two individual curve integrals.
Русский
Пусть ω интегрируем по кривым γ_{ab} и γ_{bc}. Тогда интеграл по конкатенации γ_{ab} trans γ_{bc} равен сумме интегралов по каждой кривой.
LaTeX
$$$\\text{CurveIntegrable}(\\omega, \\gamma_{ab}) \\;\\to\\; \\text{CurveIntegrable}(\\omega, \\gamma_{bc}) \\;\\to\\; \\int_{\\gamma_{ab} \\text{ trans } \\gamma_{bc}} \\omega = \\int_{\\gamma_{ab}} \\omega + \\int_{\\gamma_{bc}} \\omega$$$
Lean4
theorem curveIntegral_trans (h₁ : CurveIntegrable ω γab) (h₂ : CurveIntegrable ω γbc) :
∫ᶜ x in γab.trans γbc, ω x = (∫ᶜ x in γab, ω x) + ∫ᶜ x in γbc, ω x :=
by
let instF := NormedSpace.restrictScalars ℝ 𝕜 F
rw [curveIntegral_def, ←
intervalIntegral.integral_add_adjacent_intervals (h₁.intervalIntegrable_curveIntegralFun_trans_left γbc)
(h₂.intervalIntegrable_curveIntegralFun_trans_right γab),
intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_left _ _ _),
intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_right _ _ _)]
simp only [← ofNat_smul_eq_nsmul (R := ℝ)]
rw [intervalIntegral.integral_smul, intervalIntegral.smul_integral_comp_mul_left, intervalIntegral.integral_smul,
intervalIntegral.smul_integral_comp_mul_left (f := (curveIntegralFun ω γbc <| · - 1)),
intervalIntegral.integral_comp_sub_right]
simp only [curveIntegral_def]
norm_num
