Coarse-graining support: Support.Sobolev.W1p.InwardMollificationWeakGradient

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Weak gradient of inward mollification

This file identifies the classical coordinate derivative of the inward mollification of an H10Function with the correspondingly mollified global zero extension of its weak gradient. The proof first establishes the global convolution identity by closing the identities for the supported smooth approximants built into H10Function, and then applies the affine chain rule.

theorem HCPolySupport.H10Function.ae_eq_fderiv_inwardMollification_unit_apply_basisVec {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (hU : MeasurableSet U) {x0 : Vec d} {r ε : ℝ} (hr : 0 < r) (hε : 0 < ε) (i : Fin d) : (fun (x : Vec d) => (fderiv ℝ (inwardMollification unitConvexApproxKernel u.zeroExtension x0 r ε) x) (basisVec i)) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => (1 + ε) * MeasureTheory.convolution (scaledConvexApproxKernel unitConvexApproxKernel (ε * r)) (fun (y : Vec d) => u.zeroExtensionGrad y i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume (globalAffineExpansion x0 ε x)

The classical coordinate derivative of the inward mollification of an H¹₀ zero extension is the outward-affine pullback of the mollified weak gradient, including the exact chain-rule factor 1 + ε.