Fundamental theorem and substitution for oriented Henstock intervals

The genuine gauge FTC and substitution theorems hold for arbitrary endpoint order, including zero intervals and backtracking parametrizations. Neither theorem assumes Bochner integrability of the derivative. Constant real projections have zero integral, without curve regularity.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_of_hasDerivAt_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} {f f' : ℝ → E} {s : Set ℝ} (hs : s.Countable) (hc : ContinuousOn f (Set.uIcc a b)) (hd : ∀ x ∈ Set.uIoo a b \ s, HasDerivAt f (f' x) x) : HasHenstockIntervalIntegral f' a b (f b - f a)

The oriented Henstock fundamental theorem for a continuous primitive differentiable outside a countable exceptional set in the interval interior.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_deriv_smul_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} {f : ℝ → E} {θ θ' : ℝ → ℝ} {s : Set ℝ} (hs : s.Countable) (hθ : ContinuousOn θ (Set.uIcc a b)) (hdθ : ∀ t ∈ Set.uIoo a b \ s, HasDerivAt θ (θ' t) t) (hf : ContinuousOn f (θ '' Set.uIcc a b)) : HasHenstockIntervalIntegral (fun (t : ℝ) => θ' t • f (θ t)) a b (∫ (x : ℝ) in θ a..θ b, f x)

Oriented substitution for continuous integrands and continuous scalar parametrizations with countably many derivative exceptions. The parameter may reverse direction or backtrack.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_of_projection_constant {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (L : V →L[ℝ] ℝ) {a b c : ℝ} {γ : ℝ → V} (hγ : ∀ (t : ℝ), L (γ t) = c) (P : V → ℝ) : HasHenstockIntervalIntegral (fun (t : ℝ) => P (γ t) * L (deriv γ t)) a b 0

A raw curve with constant projection contributes zero to that coordinate one-form. No regularity of its other coordinate or of the field is needed.