English
Let the segment from a to b be parameterized by Real numbers; ω defines a curve-integrable form along this segment if and only if the associated real-interval integral of ω(lineMap(a,b,t))(b−a) over t in [0,1] is finite.
Русский
Пусть отрезок от a до b параметризован по действительным числам; интегрируемость по кривой ω вдоль этого отрезка эквивалентна тому, что соответствующий интеграл по временному параметру t ∈ [0,1] от ω(lineMap(a,b,t))(b−a) конечен.
LaTeX
$$$\\text{CurveIntegrable}(\\omega, \\text{segment}(a,b)) \\iff \\text{IntervalIntegrable}(t \\mapsto \\omega(\\text{lineMap}(a,b,t))(b-a), \\text{volume}, 0, 1)$$$
Lean4
theorem curveIntegrable_segment [NormedSpace ℝ E] :
CurveIntegrable ω (.segment a b) ↔ IntervalIntegrable (fun t ↦ ω (lineMap a b t) (b - a)) volume 0 1 :=
by
rw [CurveIntegrable, intervalIntegrable_congr]
rw [uIoc_of_le zero_le_one]
exact .mono Ioc_subset_Icc_self fun _t ↦ curveIntegralFun_segment ω a b
