Curve integrability using the ordinary derivative

The derivative within the unit interval in curveIntegralFun agrees almost everywhere with the ordinary derivative of Path.extend. Consequently curve integrability can be checked using this ordinary derivative, just as the value of the curve integral can be computed with it.

theorem TauCeti.curveIntegrable_iff_intervalIntegrable_deriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p q : E} (ω : E → E →L[𝕜] F) (γ : Path p q) : CurveIntegrable ω γ ↔ IntervalIntegrable (fun (t : ℝ) => (ω (γ.extend t)) (deriv (⇑γ.extend) t)) MeasureTheory.volume 0 1

Curve integrability is equivalent to interval integrability of the ordinary velocity paired with the 1-form. The endpoint derivative values do not affect integrability.