Coarse-graining support: #
Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.WeakDerivativeTestClosure
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.HasWeakPartialDerivOn.integral_mul_deriv_eq_neg_integral_mul_of_eLpNorm_approx
{d : ℕ}
{U : Set (Vec d)}
{i : Fin d}
{u gi ψ Dψ : Vec d → ℝ}
(huweak : HasWeakPartialDerivOn U i u gi)
(hu : MemScalarL2 U u)
(hgi : MemScalarL2 U gi)
(hψ : MemScalarL2 U ψ)
(hDψ : MemScalarL2 U Dψ)
(ψn : ℕ → Vec d → ℝ)
(hψn_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψn n))
(hψn_compact : ∀ (n : ℕ), HasCompactSupport (ψn n))
(hψn_sub : ∀ (n : ℕ), tsupport (ψn n) ⊆ U)
(hψn_mem : ∀ (n : ℕ), MemScalarL2 U (ψn n))
(hDψn_mem : ∀ (n : ℕ), MemScalarL2 U fun (x : Vec d) => euclideanCoordDeriv i (ψn n) x)
(hψn_to_ψ :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => ψn n x - ψ x) 2 (volumeMeasureOn U))
Filter.atTop (nhds 0))
(hDψn_to_Dψ :
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanCoordDeriv i (ψn n) x - Dψ x) 2 (volumeMeasureOn U))
Filter.atTop (nhds 0))
:
Extend the weak-partial-derivative identity from admissible smooth compact
tests to any test reached as an L² limit together with its coordinate
derivative.
This is the closure step needed for cube boundary tests: the geometric cutoff
argument supplies the approximating sequence ψn; this lemma performs the
functional-analytic handoff to the weak derivative identity.