MATHLIBANNEX / CANONICAL DECLARATION CARD

Zero integral of a compactly supported divergence

MathlibAnnex.Piola.integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport

theorem

Makes all faces in a box divergence formula vanish by placing the support strictly inside the box.

Statement

Fix . Let be and have compact topological support. Let denote the real Fréchet derivative and the th standard coordinate vector. Write For Lebesgue measure on the coordinate space,

Assumptions

The support convention throughout this card is This closed set is assumed compact. The differentiability hypothesis is exactly . The domain has its coordinate sup norm. No externally specified integration domain or boundary-regularity assumption is needed.

Conclusion

The divergence is integrable and its whole-space integral vanishes. Compact support is imposed on , which also forces the divergence to vanish off that support.

Notes

For the two faces are endpoints and the same formula is the fundamental theorem of calculus. The source represents face coordinates by inserting one fixed coordinate into an -tuple.

Proof route

Choose a box with the support strictly inside it. Write the box divergence formula as a sum of upper-face minus lower-face integrals. Each face value is zero, and the divergence is zero outside the box, so the whole-space integral is zero.

Proof steps

  1. Enclose the support and justify integrability. Choose such that

    If , some neighborhood of is disjoint from the nonzero set of . On that neighborhood , and hence . Therefore

    The divergence is continuous because is , so it is integrable on compact . It is zero on , and is therefore integrable on as well.

  2. Spell out the face formula. Fix . Let and write . Insert the missing coordinate by

    For fixed , the scalar function is and

    The face expression in the box divergence theorem is precisely the following repeated-integral calculation (Fubini on the compact box, followed by the one-dimensional fundamental theorem of calculus):

    Sum over to obtain . In the source this sum is obtained directly from the cited box divergence theorem: supplies continuity and a derivative everywhere, the exceptional set is empty, and Step 1 supplies integrability. The calculation above explains its face terms.

  3. Set the face values to zero and pass to the whole space. The th coordinate of is . Hence

    Each integrand in the last line of Step 2 is thus . Since Step 1 also gives on ,

    For , is the zero-dimensional one-point product; the formula is simply the difference of the two endpoint values.

Main citations

Lean source signature (exact)

theorem integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport
    {m : ℕ} {F : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}
    (hF : ContDiff ℝ 1 F) (hFc : HasCompactSupport F) :
    ∫ x, coordinateDivergence F x = 0
In the source Mathematical meaning
{m : ℕ} {F : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)} The positive dimension and vector field .
(hF : ContDiff ℝ 1 F) The exact regularity assumption is .
(hFc : HasCompactSupport F) The closed topological support is compact.
In the source Mathematical meaning
coordinateDivergence F x The function , where .
∫ x, coordinateDivergence F x = 0 The whole-space Lebesgue integral . The theorem is not merely a box integral identity.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set MeasureTheory Filter
open scoped BigOperators Topology

namespace MathlibAnnex
namespace Piola

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.Piola.integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport

Accepted content SHA-256: 6615269efd172654102c91e02a3056f51f399018a4faa42e1acd7c85d2b63488

Accepted source guide SHA-256: 9284ee529653d2155bcbe3ebf7302736c29081fc1b35539edec2dc2ff6c5bed0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑