mathlib documentation

measure_theory.integral.divergence_theorem

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

TODO #

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.

theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₁ {E : Type u} [normed_add_comm_group E] [normed_space E] [complete_space 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 : continuous_on f (box_integral.box.Icc I)) (Hd : ∀ (x : fin (n + 1)), x box_integral.box.Icc I \ shas_fderiv_within_at f (f' x) (box_integral.box.Icc I) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1)), finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 1) i)) (box_integral.box.Icc I) measure_theory.measure_space.volume) :
∫ (x : fin (n + 1)) in box_integral.box.Icc I, finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 1) i) = finset.univ.sum (λ (i : fin (n + 1)), (∫ (x : fin n) in box_integral.box.Icc (I.face i), f (i.insert_nth (I.upper i) x) i) - ∫ (x : fin n) in box_integral.box.Icc (I.face i), 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} [normed_add_comm_group E] [normed_space E] [complete_space 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 : continuous_on f (box_integral.box.Icc I)) (Hd : ∀ (x : fin (n + 1)), x box_integral.box.Ioo I \ shas_fderiv_at f (f' x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1)), finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 1) i)) (box_integral.box.Icc I) measure_theory.measure_space.volume) :
∫ (x : fin (n + 1)) in box_integral.box.Icc I, finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 1) i) = finset.univ.sum (λ (i : fin (n + 1)), (∫ (x : fin n) in box_integral.box.Icc (I.face i), f (i.insert_nth (I.upper i) x) i) - ∫ (x : fin n) in box_integral.box.Icc (I.face i), 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} [normed_add_comm_group E] [normed_space E] [complete_space 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 : continuous_on f (set.Icc a b)) (Hd : ∀ (x : fin (n + 1)), x set.univ.pi (λ (i : fin (n + 1)), set.Ioo (a i) (b i)) \ shas_fderiv_at f (f' x) x) (Hi : measure_theory.integrable_on (λ (x : fin (n + 1)), finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 1) i)) (set.Icc a b) measure_theory.measure_space.volume) :
∫ (x : fin (n + 1)) in set.Icc a b, finset.univ.sum (λ (i : fin (n + 1)), (f' x) (pi.single i 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} [normed_add_comm_group E] [normed_space E] [complete_space 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) (pi.single i 1))) (set.Icc a b) measure_theory.measure_space.volume) :
∫ (x : fin (n + 1)) in set.Icc a b, finset.univ.sum (λ (i : fin (n + 1)), (f' i x) (pi.single i 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} [normed_add_comm_group E] [normed_space E] [complete_space E] {n : } {F : Type u_1} [normed_add_comm_group F] [normed_space F] [partial_order F] [measure_theory.measure_space F] [borel_space F] (eL : F ≃L[] fin (n + 1)) (he_ord : ∀ (x y : F), eL x eL y x y) (he_vol : measure_theory.measure_preserving eL measure_theory.measure_space.volume measure_theory.measure_space.volume) (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) (pi.single i 1)))) (Hi : measure_theory.integrable_on DF (set.Icc a b) measure_theory.measure_space.volume) :
∫ (x : F) in set.Icc a 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (f f' : → E) {a b : } (hle : a b) {s : set } (hs : s.countable) (Hc : continuous_on f (set.Icc a b)) (Hd : ∀ (x : ), x set.Ioo a b \ shas_deriv_at f (f' x) x) (Hi : interval_integrable f' measure_theory.measure_space.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

theorem measure_theory.integral_eq_of_has_deriv_within_at_off_countable {E : Type u} [normed_add_comm_group E] [normed_space E] [complete_space E] (f f' : → E) {a b : } {s : set } (hs : s.countable) (Hc : continuous_on f (set.interval a b)) (Hd : ∀ (x : ), x set.Ioo (linear_order.min a b) (linear_order.max a b) \ shas_deriv_at f (f' x) x) (Hi : interval_integrable f' measure_theory.measure_space.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 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (f g : × → E) (f' g' : × ( × →L[] E)) (a b : × ) (hle : a b) (s : set ( × )) (hs : s.countable) (Hcf : continuous_on f (set.Icc a b)) (Hcg : continuous_on g (set.Icc a b)) (Hdf : ∀ (x : × ), x set.Ioo a.fst b.fst ×ˢ set.Ioo a.snd b.snd \ shas_fderiv_at f (f' x) x) (Hdg : ∀ (x : × ), x set.Ioo a.fst b.fst ×ˢ set.Ioo a.snd b.snd \ shas_fderiv_at g (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 set.Icc a 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (f g : × → E) (f' g' : × ( × →L[] E)) (a₁ a₂ b₁ b₂ : ) (s : set ( × )) (hs : s.countable) (Hcf : continuous_on f (set.interval a₁ b₁ ×ˢ set.interval a₂ b₂)) (Hcg : continuous_on g (set.interval a₁ b₁ ×ˢ set.interval a₂ b₂)) (Hdf : ∀ (x : × ), x set.Ioo (linear_order.min a₁ b₁) (linear_order.max a₁ b₁) ×ˢ set.Ioo (linear_order.min a₂ b₂) (linear_order.max a₂ b₂) \ shas_fderiv_at f (f' x) x) (Hdg : ∀ (x : × ), x set.Ioo (linear_order.min a₁ b₁) (linear_order.max a₁ b₁) ×ˢ set.Ioo (linear_order.min a₂ b₂) (linear_order.max a₂ b₂) \ shas_fderiv_at g (g' x) x) (Hi : measure_theory.integrable_on (λ (x : × ), (f' x) (1, 0) + (g' x) (0, 1)) (set.interval a₁ b₁ ×ˢ set.interval 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.