# Divergence theorem for Bochner integral #

In this file we prove the Divergence theorem for Bochner integral on a box in ℝⁿ⁺¹ = Fin (n + 1) → ℝ. More precisely, we prove the following theorem.

Let E be a complete normed space. If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is continuous on a rectangular box [a, b] : Set ℝⁿ⁺¹, a ≤ b, differentiable on its interior with derivative f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹, and the divergence fun x ↦ ∑ i, f' x eᵢ i is integrable on [a, b], where eᵢ = Pi.single i 1 is the i-th basis vector, then its integral is equal to the sum of integrals of f over the faces of [a, b], taken with appropriate signs. Moreover, the same is true if the function is not differentiable at countably many points of the interior of [a, b].

Once we prove the general theorem, we deduce corollaries for functions ℝ → E and pairs of functions (ℝ × ℝ) → E.

## Notations #

We use the following local notation to make the statement more readable. Note that the documentation website shows the actual terms, not those abbreviated using local notations.

Porting note (Yury Kudryashov): I disabled some of these notations because I failed to make them work with Lean 4.

• ℝⁿ, ℝⁿ⁺¹, Eⁿ⁺¹: Fin n → ℝ, Fin (n + 1) → ℝ, Fin (n + 1) → E;
• face i: the i-th face of the box [a, b] as a closed segment in ℝⁿ, namely [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i];
• e i : i-th basis vector Pi.single i 1;
• frontFace i, backFace i: embeddings ℝⁿ → ℝⁿ⁺¹ corresponding to the front face {x | x i = b i} and back face {x | x i = a i} of the box [a, b], respectively. They are given by Fin.insertNth i (b i) and Fin.insertNth i (a i).

## TODO #

• Add a version that assumes existence and integrability of partial derivatives.
• Restore local notations for find another way to make the statements more readable.

## Tags #

divergence theorem, Bochner integral

### Divergence theorem for functions on ℝⁿ⁺¹ = Fin (n + 1) → ℝ. #

In this section we use the divergence theorem for a Henstock-Kurzweil-like integral BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt to prove the divergence theorem for Bochner integral. The divergence theorem for Bochner integral MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable assumes that the function itself is continuous on a closed box, differentiable at all but countably many points of its interior, and the divergence is integrable on the box.

This statement differs from BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt in several aspects.

• We use Bochner integral instead of a Henstock-Kurzweil integral. This modification is done in MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁. As a side effect of this change, we need to assume that the divergence is integrable.

• We don't assume differentiability on the boundary of the box. This modification is done in MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂. To prove it, we choose an increasing sequence of smaller boxes that cover the interior of the original box, then apply the previous lemma to these smaller boxes and take the limit of both sides of the equation.

• We assume a ≤ b instead of ∀ i, a i < b i. This is the last step of the proof, and it is done in the main theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable.

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ {E : Type u} [] [] {n : } (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 : ) (Hc : ContinuousOn f (BoxIntegral.Box.Icc I)) (Hd : xBoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) (Hi : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1)) => Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) (BoxIntegral.Box.Icc I) MeasureTheory.volume) :
(∫ (x : Fin (n + 1)) in BoxIntegral.Box.Icc I, Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (∫ (x : Fin n) in BoxIntegral.Box.Icc (), f (Fin.insertNth i (I.upper i) x) i) - ∫ (x : Fin n) in BoxIntegral.Box.Icc (), f (Fin.insertNth i (I.lower i) x) i

An auxiliary lemma for MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable. This is exactly BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt reformulated for the Bochner integral.

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ {E : Type u} [] [] {n : } (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 : ) (Hc : ContinuousOn f (BoxIntegral.Box.Icc I)) (Hd : xBoxIntegral.Box.Ioo I \ s, HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1)) => Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) (BoxIntegral.Box.Icc I) MeasureTheory.volume) :
(∫ (x : Fin (n + 1)) in BoxIntegral.Box.Icc I, Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (∫ (x : Fin n) in BoxIntegral.Box.Icc (), f (Fin.insertNth i (I.upper i) x) i) - ∫ (x : Fin n) in BoxIntegral.Box.Icc (), f (Fin.insertNth i (I.lower i) x) i

An auxiliary lemma for MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable. Compared to the previous lemma, here we drop the assumption of differentiability on the boundary of the box.

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable {E : Type u} [] [] {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (hle : a b) (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 : ) (Hc : ContinuousOn f (Set.Icc a b)) (Hd : x(Set.pi Set.univ fun (i : Fin (n + 1)) => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1)) => Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) (Set.Icc a b) MeasureTheory.volume) :
(∫ (x : Fin (n + 1)) in Set.Icc a b, Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' x) () i) = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (∫ (x : Fin n) in Set.Icc () (), f (Fin.insertNth i (b i) x) i) - ∫ (x : Fin n) in Set.Icc () (), f (Fin.insertNth i (a i) x) i

Divergence theorem for Bochner integral. If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is continuous on a rectangular box [a, b] : Set ℝⁿ⁺¹, a ≤ b, is differentiable on its interior with derivative f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹ and the divergence fun x ↦ ∑ i, f' x eᵢ i is integrable on [a, b], where eᵢ = Pi.single i 1 is the i-th basis vector, then its integral is equal to the sum of integrals of f over the faces of [a, b], taken with appropriate signs.

Moreover, the same is true if the function is not differentiable at countably many points of the interior of [a, b].

We represent both faces x i = a i and x i = b i as the box face i = [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i] in ℝⁿ, where Fin.succAbove : Fin n ↪o Fin (n + 1) is the order embedding with range {i}ᶜ. The restrictions of f : ℝⁿ⁺¹ → Eⁿ⁺¹ to these faces are given by f ∘ backFace i and f ∘ frontFace i, where backFace i = Fin.insertNth i (a i) and frontFace i = Fin.insertNth i (b i) are embeddings ℝⁿ → ℝⁿ⁺¹ that take y : ℝⁿ and insert a i (resp., b i) as i-th coordinate.

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable' {E : Type u} [] [] {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (hle : a b) (f : Fin (n + 1)(Fin (n + 1))E) (f' : Fin (n + 1)(Fin (n + 1))(Fin (n + 1)) →L[] E) (s : Set (Fin (n + 1))) (hs : ) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) (Hd : x(Set.pi Set.univ fun (i : Fin (n + 1)) => Set.Ioo (a i) (b i)) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) (Hi : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1)) => Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' i x) ()) (Set.Icc a b) MeasureTheory.volume) :
(∫ (x : Fin (n + 1)) in Set.Icc a b, Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' i x) ()) = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (∫ (x : Fin n) in Set.Icc () (), f i (Fin.insertNth i (b i) x)) - ∫ (x : Fin n) in Set.Icc () (), f i (Fin.insertNth i (a i) x)

Divergence theorem for a family of functions f : Fin (n + 1) → ℝⁿ⁺¹ → E. See also MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable' for a version formulated in terms of a vector-valued function f : ℝⁿ⁺¹ → Eⁿ⁺¹.

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv {E : Type u} [] [] {n : } {F : Type u_1} [] [] [] (eL : F ≃L[] Fin (n + 1)) (he_ord : ∀ (x y : F), eL x eL y x y) (he_vol : MeasureTheory.MeasurePreserving (eL) MeasureTheory.volume MeasureTheory.volume) (f : Fin (n + 1)FE) (f' : Fin (n + 1)FF →L[] E) (s : Set F) (hs : ) (a : F) (b : F) (hle : a b) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) (Hd : xinterior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) (DF : FE) (hDF : ∀ (x : F), DF x = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (f' i x) ( ())) (Hi : MeasureTheory.IntegrableOn DF (Set.Icc a b) MeasureTheory.volume) :
∫ (x : F) in Set.Icc a b, DF x = Finset.sum Finset.univ fun (i : Fin (n + 1)) => (∫ (x : Fin n) in Set.Icc (eL a ) (eL b ), f i ( (Fin.insertNth i (eL b i) x))) - ∫ (x : Fin n) in Set.Icc (eL a ) (eL b ), f i ( (Fin.insertNth i (eL a i) x))

An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do not have the form Fin n → ℝ.

theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le {E : Type u} [] [] (f : E) (f' : E) {a : } {b : } (hle : a b) {s : } (hs : ) (Hc : ContinuousOn f (Set.Icc a b)) (Hd : xSet.Ioo a b \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (x : ) in a..b, f' x = f b - f a

Fundamental theorem of calculus, part 2. This version assumes that f is continuous on the interval and is differentiable off a countable set s.

• intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le for a version that only assumes right differentiability of f;

• MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable for a version that works both for a ≤ b and b ≤ a at the expense of using unordered intervals instead of Set.Icc.

theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable {E : Type u} [] [] (f : E) (f' : E) {a : } {b : } {s : } (hs : ) (Hc : ContinuousOn f (Set.uIcc a b)) (Hd : xSet.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (x : ) in a..b, f' x = f b - f a

Fundamental theorem of calculus, part 2. This version assumes that f is continuous on the interval and is differentiable off a countable set s.

See also intervalIntegral.integral_eq_sub_of_hasDeriv_right for a version that only assumes right differentiability of f.

theorem MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le {E : Type u} [] [] (f : E) (g : E) (f' : →L[] E) (g' : →L[] E) (a : ) (b : ) (hle : a b) (s : Set ()) (hs : ) (Hcf : ContinuousOn f (Set.Icc a b)) (Hcg : ContinuousOn g (Set.Icc a b)) (Hdf : xSet.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x) (Hdg : xSet.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x) (Hi : MeasureTheory.IntegrableOn (fun (x : ) => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) MeasureTheory.volume) :
∫ (x : ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) = (((∫ (x : ) in a.1 ..b.1, g (x, b.2)) - ∫ (x : ) in a.1 ..b.1, g (x, a.2)) + ∫ (y : ) in a.2 ..b.2, f (b.1, y)) - ∫ (y : ) in a.2 ..b.2, f (a.1, y)

Divergence theorem for functions on the plane along rectangles. It is formulated in terms of two functions f g : ℝ × ℝ → E and an integral over Icc a b = [a.1, b.1] × [a.2, b.2], where a b : ℝ × ℝ, a ≤ b. When thinking of f and g as the two coordinates of a single function F : ℝ × ℝ → E × E and when E = ℝ, this is the usual statement that the integral of the divergence of F inside the rectangle equals the integral of the normal derivative of F along the boundary.

See also MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable for a version that does not assume a ≤ b and uses iterated interval integral instead of the integral over Icc a b.

theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable {E : Type u} [] [] (f : E) (g : E) (f' : →L[] E) (g' : →L[] E) (a₁ : ) (a₂ : ) (b₁ : ) (b₂ : ) (s : Set ()) (hs : ) (Hcf : ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hcg : ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hdf : xSet.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) (Hdg : xSet.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) (Hi : MeasureTheory.IntegrableOn (fun (x : ) => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) MeasureTheory.volume) :
∫ (x : ) in a₁..b₁, ∫ (y : ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ) in a₁..b₁, g (x, b₂)) - ∫ (x : ) in a₁..b₁, g (x, a₂)) + ∫ (y : ) in a₂..b₂, f (b₁, y)) - ∫ (y : ) in a₂..b₂, f (a₁, y)

Divergence theorem for functions on the plane. It is formulated in terms of two functions f g : ℝ × ℝ → E and iterated integral ∫ x in a₁..b₁, ∫ y in a₂..b₂, _, where a₁ a₂ b₁ b₂ : ℝ. When thinking of f and g as the two coordinates of a single function F : ℝ × ℝ → E × E and when E = ℝ, this is the usual statement that the integral of the divergence of F inside the rectangle with vertices (aᵢ, bⱼ), i, j =1,2, equals the integral of the normal derivative of F along the boundary.

See also MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le for a version that uses an integral over Icc a b, where a b : ℝ × ℝ, a ≤ b.