English
The integral of a 1-form along a path γ is defined as the Bochner integral of the curve integral function along γ from 0 to 1.
Русский
Интеграл 1-формы вдоль пути γ задаётся как Бо́хнеров интеграл функции curveIntegralFun γ от 0 до 1.
LaTeX
$$$ \\curveIntegral(\\omega, \\gamma) = \\int_{0}^{1} \\curveIntegralFun(\\omega, \\gamma, t) \\, dt $$$
Lean4
/-- Integral of a 1-form `ω : E → E →L[𝕜] F` along a path `γ`,
defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$.
The actual definition uses `curveIntegralFun` which uses `Path.extend γ`
and `derivWithin (Path.extend γ) (Set.Icc 0 1) t`,
because calculus-related definitions in Mathlib expect globally defined functions as arguments. -/
noncomputable def curveIntegral :=
val_proj @wrapped✝.{}
