English
A 1-form ω is curve integrable along a path γ if the function t ↦ curveIntegralFun ω γ t is integrable on the interval [0,1].
Русский
1-форма ω по кривой γ интегрируема тогда, когда функция t ↦ curveIntegralFun ω γ t интегрируема на интервале [0,1].
LaTeX
$$$ \\text{CurveIntegrable}(\\omega, \\gamma) \\iff \\text{IntervalIntegrable}(\\curveIntegralFun(\\omega, \\gamma), \\mathrm{volume}, 0, 1) $$$
Lean4
/-- A 1-form `ω` is *curve integrable* along a path `γ`,
if the function `curveIntegralFun ω γ t = ω (γ t) (γ' t)` is integrable on `[0, 1]`.
The actual definition uses `Path.extend γ`,
because both interval integrals and derivatives expect globally defined functions.
-/
def CurveIntegrable (ω : E → E →L[𝕜] F) (γ : Path a b) : Prop :=
IntervalIntegrable (curveIntegralFun ω γ) volume 0 1
