curveIntegral_segment — Mathlib

English

If ω is a fixed linear map constant along the segment from a to b, the curve integral over the segment equals ω(b − a).

Русский

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

LaTeX

$$$\\text{curveIntegral}(\\omega, \\text{segment}(a,b)) = \\omega(b-a)$$$

Lean4

theorem curveIntegral_segment [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (a b : E) :
    ∫ᶜ x in .segment a b, ω x = ∫ t in 0..1, ω (lineMap a b t) (b - a) :=
  by
  rw [curveIntegral_def]
  refine intervalIntegral.integral_congr fun t ht ↦ ?_
  rw [uIcc_of_le zero_le_one] at ht
  exact curveIntegralFun_segment ω a b ht

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