Agreement of Henstock and Bochner curve integrals #
Mathlib's CurveIntegrable supplies genuine Bochner integrability of curveIntegralFun.
Its Henstock integral therefore has the same value as Mathlib's curveIntegral, by the
oriented interval compatibility theorem. The comparison retains the integrability hypothesis.
Constant-projection paths have zero Henstock coordinate integral without regularity assumptions.
theorem
CurveIntegrable.hasHenstockIntervalIntegral
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{a b : E}
{ω : E → E →L[𝕜] F}
{γ : Path a b}
(h : CurveIntegrable ω γ)
:
have this := NormedSpace.restrictScalars ℝ 𝕜 F;
TauCeti.BoxIntegral.HasHenstockIntervalIntegral (curveIntegralFun ω γ) 0 1 (curveIntegral ω γ)
A Bochner-integrable one-form along a path has its actual curve-integral value as a Henstock integral of Mathlib's curve integrand on the unit parameter interval.
theorem
TauCeti.BoxIntegral.HasHenstockIntervalIntegral.eq_curveIntegral
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{a b : E}
{ω : E → E →L[𝕜] F}
{γ : Path a b}
{y : F}
(h : HasHenstockIntervalIntegral (curveIntegralFun ω γ) 0 1 y)
(hω : CurveIntegrable ω γ)
:
Under genuine curve integrability, any Henstock value of Mathlib's curve integrand agrees with its Bochner curve integral.
theorem
TauCeti.BoxIntegral.hasIntegral_Henstock_of_path_projection_constant
{V : Type u_4}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(L : V →L[ℝ] ℝ)
{p q : V}
(γ : Path p q)
(hγ : ∀ (t : ↑unitInterval), L (γ t) = L p)
(P : V → ℝ)
:
BoxIntegral.HasIntegral (intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock
(fun (t : Fin 1 → ℝ) => P (γ.extend (t 0)) * L (deriv (⇑γ.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume 0
Every path with constant selected coordinate has zero gauge coordinate integral.