Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.W10pWeakTestClosure #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.CubeCalderonZygmund.weak_divergence_identity_of_w10p
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)]
(p : FiniteLpExponent)
(hp : 2 ≤ p.exponent)
(w : H1Function U)
(h : Vec d → Vec d)
(hh : MemVectorL2 U h)
(sigma0 : ℝ)
(hweak :
∀ (phi : Vec d → ℝ),
ContDiff ℝ (↑⊤) phi →
HasCompactSupport phi →
tsupport phi ⊆ U →
sigma0 * ∫ (x : Vec d) in U, vecDot (w.grad x) (euclideanGradient phi x) = -∫ (x : Vec d) in U, vecDot (h x) (euclideanGradient phi x))
(v : W10pFunction U p.exponent)
:
Extend a smooth compactly supported weak-divergence identity to every
zero-trace W^{1,p} test on a finite-measure domain when p ≥ 2.