English
The curved integral equals the interval integral of a function involving γ^{extend} and its derivative along the interval.
Русский
Криволинейный интеграл равен интегралу по [0,1] функции, зависящей от γ^{extend} и её производной.
LaTeX
$$$ \\curveIntegral(\\omega, \\gamma) = \\int_{0}^{1} \\omega\\bigl(\\gamma^{\\mathrm{extend}}(t)\\bigr)\\bigl(\\derivWithin(\\gamma^{\\mathrm{extend}}, \\mathrm{I}, t)\\bigr) \\, dt $$$
Lean4
theorem curveIntegral_eq_intervalIntegral_deriv [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b) :
∫ᶜ x in γ, ω x = ∫ t in 0..1, ω (γ.extend t) (deriv γ.extend t) :=
by
simp only [curveIntegral_def, curveIntegralFun_def]
apply intervalIntegral.integral_congr_ae_restrict
rw [uIoc_of_le zero_le_one, ← restrict_Ioo_eq_restrict_Ioc]
filter_upwards [ae_restrict_mem (by measurability)] with x hx
rw [derivWithin_of_mem_nhds (by simpa)]
