Compactly supported divergence on a vector space #
This specializes Mathlib's MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
to a globally C¹, compactly supported vector field. A bounding box contains its support,
so every boundary flux vanishes and the full-space divergence integral is zero.
It also localizes the divergence integral over a set of unique differentiability to a box containing the part of the support inside that set, which the half-space and quadrant divergence theorems share.
theorem
ContDiffOn.integrableOn_divergence_and_setIntegral_eq_Icc
{n : ℕ}
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : (Fin (n + 1) → ℝ) → Fin (n + 1) → F}
{s : Set (Fin (n + 1) → ℝ)}
(hf : ContDiffOn ℝ 1 f s)
(hs : UniqueDiffOn ℝ s)
(hsm : MeasurableSet s)
{a b : Fin (n + 1) → ℝ}
(hab : Set.Icc a b ⊆ s)
(hsupp : ∀ x ∈ s, x ∈ tsupport f → x ∈ Set.Icc a b)
:
MeasureTheory.IntegrableOn (fun (x : Fin (n + 1) → ℝ) => ∑ i : Fin (n + 1), (fderivWithin ℝ f s x) (Pi.single i 1) i)
(Set.Icc a b) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Fin (n + 1) → ℝ) => ∑ i : Fin (n + 1), (fderivWithin ℝ f s x) (Pi.single i 1) i)
s MeasureTheory.volume ∧ ∫ (x : Fin (n + 1) → ℝ) in s, ∑ i : Fin (n + 1), (fderivWithin ℝ f s x) (Pi.single i 1) i = ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), (fderivWithin ℝ f s x) (Pi.single i 1) i
Let f be C¹ on a measurable set s of unique differentiability, and let the part of its
support inside s lie in a box Icc a b ⊆ s. Then its divergence within s is integrable on the
box and on s, and its integrals over both agree.