# 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

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

Auxiliary lemma for the divergence theorem.

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

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