Documentation

Mathlib.MeasureTheory.Integral.DivergenceTheorem

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.

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

theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {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 : s.Countable) (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)) => i : Fin (n + 1), (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I) MeasureTheory.volume) :
∫ (x : Fin (n + 1)) in BoxIntegral.Box.Icc I, i : Fin (n + 1), (f' x) (Pi.single i 1) i = i : Fin (n + 1), ((∫ (x : Fin n) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {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 : s.Countable) (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)) => i : Fin (n + 1), (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I) MeasureTheory.volume) :
∫ (x : Fin (n + 1)) in BoxIntegral.Box.Icc I, i : Fin (n + 1), (f' x) (Pi.single i 1) i = i : Fin (n + 1), ((∫ (x : Fin n) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {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 : s.Countable) (Hc : ContinuousOn f (Set.Icc a b)) (Hd : x(Set.univ.pi 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)) => i : Fin (n + 1), (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume) :
∫ (x : Fin (n + 1)) in Set.Icc a b, i : Fin (n + 1), (f' x) (Pi.single i 1) i = i : Fin (n + 1), ((∫ (x : Fin n) in Set.Icc (a i.succAbove) (b i.succAbove), f (i.insertNth (b i) x) i) - ∫ (x : Fin n) in Set.Icc (a i.succAbove) (b i.succAbove), f (i.insertNth (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {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 : s.Countable) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) (Hd : x(Set.univ.pi 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)) => i : Fin (n + 1), (f' i x) (Pi.single i 1)) (Set.Icc a b) MeasureTheory.volume) :
∫ (x : Fin (n + 1)) in Set.Icc a b, i : Fin (n + 1), (f' i x) (Pi.single i 1) = i : Fin (n + 1), ((∫ (x : Fin n) in Set.Icc (a i.succAbove) (b i.succAbove), f i (i.insertNth (b i) x)) - ∫ (x : Fin n) in Set.Icc (a i.succAbove) (b i.succAbove), f i (i.insertNth (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {n : } {F : Type u_1} [NormedAddCommGroup F] [NormedSpace F] [PartialOrder F] [MeasureTheory.MeasureSpace F] [BorelSpace F] (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 : s.Countable) (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 = i : Fin (n + 1), (f' i x) (eL.symm (Pi.single i 1))) (Hi : MeasureTheory.IntegrableOn DF (Set.Icc a b) MeasureTheory.volume) :
∫ (x : F) in Set.Icc a b, DF x = i : Fin (n + 1), ((∫ (x : Fin n) in Set.Icc (eL a i.succAbove) (eL b i.succAbove), f i (eL.symm (i.insertNth (eL b i) x))) - ∫ (x : Fin n) in Set.Icc (eL a i.succAbove) (eL b i.succAbove), f i (eL.symm (i.insertNth (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (f' : E) {a : } {b : } (hle : a b) {s : Set } (hs : s.Countable) (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.

See also

theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (f' : E) {a : } {b : } {s : Set } (hs : s.Countable) (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : × E) (g : × E) (f' : × × →L[] E) (g' : × × →L[] E) (a : × ) (b : × ) (hle : a b) (s : Set ( × )) (hs : s.Countable) (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} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : × E) (g : × E) (f' : × × →L[] E) (g' : × × →L[] E) (a₁ : ) (a₂ : ) (b₁ : ) (b₂ : ) (s : Set ( × )) (hs : s.Countable) (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.