Curve integrals along a fixed affine line

Straight segments on one affine line are exactly oriented interval integrals of the same one-dimensional coefficient. This permits cancellation even when the line parameters reverse direction or coincide.

theorem TauCeti.curveIntegral_segment_line {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ω : E → E →L[ℝ] F) (c v : E) (a b : ℝ) : curveIntegral ω (Path.segment (c + a • v) (c + b • v)) = ∫ (t : ℝ) in a..b, (ω (c + t • v)) v

The integral along a segment on a fixed affine line is the oriented interval integral in its real line coordinate. No ordering of the two parameters is required.