The Henstock–Kurzweil fundamental theorem of calculus

The GP integral agrees with the Henstock–Kurzweil integral on one-dimensional boxes. For a continuous Banach-valued function f with derivative f' outside a countable exceptional set, the Henstock–Kurzweil integral of f' equals f b - f a. The derivative need not be Bochner integrable, and its values at the exceptions are arbitrary.

The FTC is derived from Mathlib's BoxIntegral.hasIntegral_GP_pderiv using the GP–Henstock equivalence in dimension one. Finite exceptional sets, such as break points of piecewise differentiable parametrizations, are a special case of the countable hypothesis.

@[simp]

theorem BoxIntegral.Box.distortion_of_unique {ι : Type u_1} [Fintype ι] [Unique ι] (I : Box ι) : I.distortion = 1

Every nondegenerate one-dimensional box has distortion one.

theorem TauCeti.BoxIntegral.hasIntegral_GP_iff_Henstock_of_unique {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [Unique ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F} : BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP f vol y ↔ BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.Henstock f vol y

On a finite unique-coordinate box the GP distortion restriction imposes no extra condition.

theorem TauCeti.BoxIntegral.hasIntegral_GP_iff_Henstock_fin_one {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : BoxIntegral.Box (Fin 1)} {f : (Fin 1 → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap (Fin 1) (E →L[ℝ] F) ⊤} {y : F} : BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP f vol y ↔ BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.Henstock f vol y

In dimension one the GP and Henstock integrals coincide. This is the interval-coordinate specialization used by the Henstock FTC.

theorem TauCeti.BoxIntegral.hasIntegral_Henstock_of_hasDerivWithinAt_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a < b) {f f' : ℝ → E} {s : Set ℝ} (hs : s.Countable) (hc : ContinuousOn f (Set.Icc a b)) (hd : ∀ x ∈ Set.Icc a b \ s, HasDerivWithinAt f (f' x) (Set.Icc a b) x) : BoxIntegral.HasIntegral (intervalBox a b hab) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f' (x 0)) BoxIntegral.BoxAdditiveMap.volume (f b - f a)

Henstock–Kurzweil FTC for continuous Banach-valued primitives, with a countable exceptional set. There is no integrability or boundedness requirement on the derivative; its values on the exceptional set do not affect the integral.

theorem TauCeti.BoxIntegral.hasIntegral_Henstock_of_hasDerivAt_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a < b) {f f' : ℝ → E} {s : Set ℝ} (hs : s.Countable) (hc : ContinuousOn f (Set.Icc a b)) (hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x) : BoxIntegral.HasIntegral (intervalBox a b hab) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f' (x 0)) BoxIntegral.BoxAdditiveMap.volume (f b - f a)

Henstock–Kurzweil FTC assuming differentiability only in the interior, outside a countable exceptional set. No derivative is required at either endpoint.