curveIntegralFun_segment — Mathlib

English

For a segment from a to b, the curve integral of ω along the segment at parameter t equals ω(lineMap(a,b,t)) applied to the tangent (b−a).

Русский

Для отрезка от a до b интеграл по кривой ω вдоль отрезка в параметр t равен ω(lineMap(a,b,t)) применяемому к вектору b−a.

LaTeX

$$$\\text{curveIntegralFun}(\\omega, \\text{segment}(a,b), t) = \\omega(\\text{lineMap}(a,b,t))(b-a)$$$

Lean4

theorem curveIntegralFun_segment [NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (a b : E) {t : ℝ} (ht : t ∈ I) :
    curveIntegralFun ω (.segment a b) t = ω (lineMap a b t) (b - a) :=
  by
  have := Path.eqOn_extend_segment a b
  simp only [curveIntegralFun_def, this ht, derivWithin_congr this (this ht),
    (hasDerivWithinAt_lineMap ..).derivWithin (uniqueDiffOn_Icc_zero_one t ht)]

Похожие утверждения