The mollified weak-derivative identity as an explicit integral

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. Integrating the derivative of the normalized bump kernel against u reproduces the mollification of a weak partial derivative of u, at every point whose closed ε-ball lies in the domain of the weak derivative. The result is the integral form of the transport identity, stated on its own so that it can be used without unfolding the convolution derivative.

theorem CKN.integral_fderiv_mollifier_mul_eq_mollify {d : ℕ} {U : Set (Vec d)} {u gi : Vec d → ℝ} {i : Fin d} : MeasureTheory.LocallyIntegrable u MeasureTheory.volume → MeasureTheory.LocallyIntegrable gi MeasureTheory.volume → ∀ (hweak : HasWeakPartialDerivOn U i u gi) {ε : ℝ} (hε : 0 < ε) {x : Vec d} (hx : Metric.closedBall x ε ⊆ U), ∫ (y : Vec d), (fderiv ℝ (mollifier ε hε) y) (basisVec i) * u (x - y) = mollify gi ε hε x

Integrating the mollifier's derivative against u reproduces the mollification of a weak partial derivative gi of u, at every point whose closed ε-ball lies in the domain.