Divergence integral for Henstock-Kurzweil integral

In this file we prove the Divergence Theorem for a Henstock-Kurzweil style integral. The theorem says the following. Let f : ℝⁿ → Eⁿ be a function differentiable on a closed rectangular box I with derivative f' x : ℝⁿ →L[ℝ] Eⁿ at x ∈ I. Then the divergence fun x ↦ ∑ k, f' x eₖ k, where eₖ = Pi.single k 1 is the k-th basis vector, is integrable on I, and its integral is equal to the sum of integrals of f over the faces of I taken with appropriate signs.

To make the proof work, we had to ban tagged partitions with “long and thin” boxes. More precisely, we use the following generalization of one-dimensional Henstock-Kurzweil integral to functions defined on a box in ℝⁿ (it corresponds to the value BoxIntegral.IntegrationParams.GP = ⊥ of BoxIntegral.IntegrationParams in the definition of BoxIntegral.HasIntegral).

We say that f : ℝⁿ → E has integral y : E over a box I ⊆ ℝⁿ if for an arbitrarily small positive ε and an arbitrarily large c, there exists a function r : ℝⁿ → (0, ∞) such that for any tagged partition π of I such that

• π is a Henstock partition, i.e., each tag belongs to its box;
• π is subordinate to r;
• for every box of π, the maximum of the ratios of its sides is less than or equal to c,

the integral sum of f over π is ε-close to y. In case of dimension one, the last condition trivially holds for any c ≥ 1, so this definition is equivalent to the standard definition of Henstock-Kurzweil integral.

Tags

Henstock-Kurzweil integral, integral, Stokes theorem, divergence theorem

theorem BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} [CompleteSpace E] (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {f : (Fin (n + 1) → ℝ) → E} {f' : (Fin (n + 1) → ℝ) →L[ℝ] E} (hfc : ContinuousOn f (↑BoxIntegral.Box.Icc I)) {x : Fin (n + 1) → ℝ} (hxI : x ∈ ↑BoxIntegral.Box.Icc I) {a : E} {ε : ℝ} (h0 : 0 < ε) (hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑BoxIntegral.Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖) {c : NNReal} (hc : BoxIntegral.Box.distortion I ≤ c) : ‖(Finset.prod Finset.univ fun j => BoxIntegral.Box.upper I j - BoxIntegral.Box.lower I j) • ↑f' (Pi.single i 1) - (BoxIntegral.integral (BoxIntegral.Box.face I i) ⊥ (f ∘ Fin.insertNth i (BoxIntegral.Box.upper I i)) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (BoxIntegral.Box.face I i) ⊥ (f ∘ Fin.insertNth i (BoxIntegral.Box.lower I i)) BoxIntegral.BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * Finset.prod Finset.univ fun j => BoxIntegral.Box.upper I j - BoxIntegral.Box.lower I j

Auxiliary lemma for the divergence theorem.

theorem BoxIntegral.hasIntegral_GP_pderiv {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} [CompleteSpace E] (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ)) (hs : Set.Countable s) (Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑BoxIntegral.Box.Icc I) x) (Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑BoxIntegral.Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑BoxIntegral.Box.Icc I) x) (i : Fin (n + 1)) : BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => ↑(f' x) (Pi.single i 1)) BoxIntegral.BoxAdditiveMap.volume (BoxIntegral.integral (BoxIntegral.Box.face I i) BoxIntegral.IntegrationParams.GP (fun x => f (Fin.insertNth i (BoxIntegral.Box.upper I i) x)) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (BoxIntegral.Box.face I i) BoxIntegral.IntegrationParams.GP (fun x => f (Fin.insertNth i (BoxIntegral.Box.lower I i) x)) BoxIntegral.BoxAdditiveMap.volume)

If f : ℝⁿ⁺¹ → E is differentiable on a closed rectangular box I with derivative f', then the partial derivative fun x ↦ f' x (Pi.single i 1) is Henstock-Kurzweil integrable with integral equal to the difference of integrals of f over the faces x i = I.upper i and x i = I.lower i.

More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and we allow f to be non-differentiable (but still continuous) at a countable set of points.

TODO: If n > 0, then the condition at x ∈ s can be replaced by a much weaker estimate but this requires either better integrability theorems, or usage of a filter depending on the countable set s (we need to ensure that none of the faces of a partition contain a point from s).

theorem BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} [CompleteSpace E] (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)) (hs : Set.Countable s) (Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑BoxIntegral.Box.Icc I) x) (Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑BoxIntegral.Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑BoxIntegral.Box.Icc I) x) : BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => Finset.sum Finset.univ fun i => ↑(f' x) (Pi.single i 1) i) BoxIntegral.BoxAdditiveMap.volume (Finset.sum Finset.univ fun i => BoxIntegral.integral (BoxIntegral.Box.face I i) BoxIntegral.IntegrationParams.GP (fun x => f (Fin.insertNth i (BoxIntegral.Box.upper I i) x) i) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (BoxIntegral.Box.face I i) BoxIntegral.IntegrationParams.GP (fun x => f (Fin.insertNth i (BoxIntegral.Box.lower I i) x) i) BoxIntegral.BoxAdditiveMap.volume)

Divergence theorem for a Henstock-Kurzweil style integral.

If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is differentiable on a closed rectangular box I with derivative f', then the divergence ∑ i, f' x (Pi.single i 1) i is Henstock-Kurzweil integrable with integral equal to the sum of integrals of f over the faces of I taken with appropriate signs.

More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and we allow f to be non-differentiable (but still continuous) at a countable set of points.