# mathlib3documentation

measure_theory.integral.divergence_theorem

# Divergence theorem for Bochner integral #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 λ 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.

• ℝⁿ, ℝⁿ⁺¹, 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.succ_above i, b ∘ fin.succ_above i];
• e i : i-th basis vector pi.single i 1;
• front_face i, back_face 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.insert_nth i (b i) and fin.insert_nth i (a i).

## TODO #

• Add a version that assumes existence and integrability of partial derivatives.

## 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 box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at to prove the divergence theorem for Bochner integral. The divergence theorem for Bochner integral measure_theory.integral_divergence_of_has_fderiv_within_at_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 box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at in several aspects.

• We use Bochner integral instead of a Henstock-Kurzweil integral. This modification is done in measure_theory.integral_divergence_of_has_fderiv_within_at_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 measure_theory.integral_divergence_of_has_fderiv_within_at_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 measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable.

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₁ {E : Type u} [ E] {n : } (I : box_integral.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) (Hc : ) (Hd : (x : fin (n + 1) ), x (f' x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1) ), finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i)) measure_theory.measure_space.volume) :
(x : fin (n + 1) ) in , finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i) = finset.univ.sum (λ (i : fin (n + 1)), ( (x : fin n ) in , f (i.insert_nth (I.upper i) x) i) - (x : fin n ) in , f (i.insert_nth (I.lower i) x) i)

An auxiliary lemma for measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable. This is exactly box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at reformulated for the Bochner integral.

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₂ {E : Type u} [ E] {n : } (I : box_integral.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) (Hc : ) (Hd : (x : fin (n + 1) ), x (f' x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1) ), finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i)) measure_theory.measure_space.volume) :
(x : fin (n + 1) ) in , finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i) = finset.univ.sum (λ (i : fin (n + 1)), ( (x : fin n ) in , f (i.insert_nth (I.upper i) x) i) - (x : fin n ) in , f (i.insert_nth (I.lower i) x) i)

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

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable {E : Type u} [ E] {n : } (a 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 : s.countable) (Hc : (set.Icc a b)) (Hd : (x : fin (n + 1) ), x set.univ.pi (λ (i : fin (n + 1)), set.Ioo (a i) (b i)) \ s (f' x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1) ), finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i)) (set.Icc a b) measure_theory.measure_space.volume) :
(x : fin (n + 1) ) in b, finset.univ.sum (λ (i : fin (n + 1)), (f' x) 1) i) = finset.univ.sum (λ (i : fin (n + 1)), ( (x : fin n ) in set.Icc (a (i.succ_above)) (b (i.succ_above)), f (i.insert_nth (b i) x) i) - (x : fin n ) in set.Icc (a (i.succ_above)) (b (i.succ_above)), f (i.insert_nth (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 λ 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 appropriat 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.succ_above i, b ∘ fin.succ_above i] in ℝⁿ, where fin.succ_above : 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 ∘ back_face i and f ∘ front_face i, where back_face i = fin.insert_nth i (a i) and front_face i = fin.insert_nth i (b i) are embeddings ℝⁿ → ℝⁿ⁺¹ that take y : ℝⁿ and insert a i (resp., b i) as i-th coordinate.

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable' {E : Type u} [ E] {n : } (a 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 : s.countable) (Hc : (i : fin (n + 1)), continuous_on (f i) (set.Icc a b)) (Hd : (x : fin (n + 1) ), x set.univ.pi (λ (i : fin (n + 1)), set.Ioo (a i) (b i)) \ s (i : fin (n + 1)), has_fderiv_at (f i) (f' i x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1) ), finset.univ.sum (λ (i : fin (n + 1)), (f' i x) 1))) (set.Icc a b) measure_theory.measure_space.volume) :
(x : fin (n + 1) ) in b, finset.univ.sum (λ (i : fin (n + 1)), (f' i x) 1)) = finset.univ.sum (λ (i : fin (n + 1)), ( (x : fin n ) in set.Icc (a (i.succ_above)) (b (i.succ_above)), f i (i.insert_nth (b i) x)) - (x : fin n ) in set.Icc (a (i.succ_above)) (b (i.succ_above)), f i (i.insert_nth (a i) x))

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

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_of_equiv {E : Type u} [ E] {n : } {F : Type u_1} [ F] [borel_space F] (eL : F ≃L[] fin (n + 1) ) (he_ord : (x y : F), eL x eL y x y) (f : fin (n + 1) F E) (f' : fin (n + 1) F (F →L[] E)) (s : set F) (hs : s.countable) (a b : F) (hle : a b) (Hc : (i : fin (n + 1)), continuous_on (f i) (set.Icc a b)) (Hd : (x : F), x interior (set.Icc a b) \ s (i : fin (n + 1)), has_fderiv_at (f i) (f' i x) x) (DF : F E) (hDF : (x : F), DF x = finset.univ.sum (λ (i : fin (n + 1)), (f' i x) ((eL.symm) 1))))  :
(x : F) in b, DF x = finset.univ.sum (λ (i : fin (n + 1)), ( (x : fin n ) in set.Icc (eL a (i.succ_above)) (eL b (i.succ_above)), f i ((eL.symm) (i.insert_nth (eL b i) x))) - (x : fin n ) in set.Icc (eL a (i.succ_above)) (eL b (i.succ_above)), f i ((eL.symm) (i.insert_nth (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 measure_theory.integral_eq_of_has_deriv_within_at_off_countable_of_le {E : Type u} [ E] (f f' : E) {a b : } (hle : a b) {s : set } (hs : s.countable) (Hc : (set.Icc a b)) (Hd : (x : ), x b \ s (f' x) x)  :
(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.

• interval_integral.integral_eq_sub_of_has_deriv_right_of_le for a version that only assumes right differentiability of f;

• measure_theory.integral_eq_of_has_deriv_within_at_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 measure_theory.integral_eq_of_has_deriv_within_at_off_countable {E : Type u} [ E] (f f' : E) {a b : } {s : set } (hs : s.countable) (Hc : (set.uIcc a b)) (Hd : (x : ), x set.Ioo b) b) \ s (f' x) x)  :
(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 measure_theory.interval_integral.integral_eq_sub_of_has_deriv_right for a version that only assumes right differentiability of f.

theorem measure_theory.integral_divergence_prod_Icc_of_has_fderiv_within_at_off_countable_of_le {E : Type u} [ E] (f g : E) (f' g' : ( × →L[] E)) (a b : × ) (hle : a b) (s : set ( × )) (hs : s.countable) (Hcf : (set.Icc a b)) (Hcg : (set.Icc a b)) (Hdf : (x : × ), x b.fst ×ˢ b.snd \ s (f' x) x) (Hdg : (x : × ), x b.fst ×ˢ b.snd \ s (g' x) x) (Hi : measure_theory.integrable_on (λ (x : × ), (f' x) (1, 0) + (g' x) (0, 1)) (set.Icc a b) measure_theory.measure_space.volume) :
(x : × ) in b, (f' x) (1, 0) + (g' x) (0, 1) = ((( (x : ) in a.fst..b.fst, g (x, b.snd)) - (x : ) in a.fst..b.fst, g (x, a.snd)) + (y : ) in a.snd..b.snd, f (b.fst, y)) - (y : ) in a.snd..b.snd, f (a.fst, 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 measure_theory.integral2_divergence_prod_of_has_fderiv_within_at_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 measure_theory.integral2_divergence_prod_of_has_fderiv_within_at_off_countable {E : Type u} [ E] (f g : E) (f' g' : ( × →L[] E)) (a₁ a₂ b₁ b₂ : ) (s : set ( × )) (hs : s.countable) (Hcf : (set.uIcc a₁ b₁ ×ˢ set.uIcc a₂ b₂)) (Hcg : (set.uIcc a₁ b₁ ×ˢ set.uIcc a₂ b₂)) (Hdf : (x : × ), x set.Ioo b₁) b₁) ×ˢ set.Ioo b₂) b₂) \ s (f' x) x) (Hdg : (x : × ), x set.Ioo b₁) b₁) ×ˢ set.Ioo b₂) b₂) \ s (g' x) x) (Hi : measure_theory.integrable_on (λ (x : × ), (f' x) (1, 0) + (g' x) (0, 1)) (set.uIcc a₁ b₁ ×ˢ set.uIcc a₂ b₂) measure_theory.measure_space.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 measure_theory.integral_divergence_prod_Icc_of_has_fderiv_within_at_off_countable_of_le for a version that uses an integral over Icc a b, where a b : ℝ × ℝ, a ≤ b.