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.
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: thei-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 vectorPi.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 byFin.insertNth i (b i)andFin.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 ≤ binstead of∀ i, a i < b i. This is the last step of the proof, and it is done in the main theoremMeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable.
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.
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.
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.
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ⁿ⁺¹.
An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do
not have the form Fin n → ℝ.
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
-
interval_integral.integral_eq_sub_of_has_deriv_right_of_lefor a version that only assumes right differentiability off; -
MeasureTheory.integral_eq_of_has_deriv_within_at_off_countablefor a version that works both fora ≤ bandb ≤ aat the expense of using unordered intervals instead ofSet.Icc.
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.
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.
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.