Interior transport of weak derivatives through mollification

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. The translated ContDiffBump is used as the test function in the defining weak-derivative identity, while Mathlib supplies the convolution derivative and measure-preserving change of variables.

The transport theorem below is pointwise on a closed-ball interior condition, with a compact-set wrapper. The general local L^p approximation theorem is not asserted here because the available Mathlib API does not provide the needed local convolution bound and translation-continuity package.

theorem CKN.fderiv_mollify_eq_mollify_of_hasWeakPartialDerivOn {d : ℕ} {U : Set (Vec d)} : IsOpen U → ∀ {u gi : Vec d → ℝ} {i : Fin d} (hu : 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), (fderiv ℝ (mollify u ε hε) x) (basisVec i) = mollify gi ε hε x

theorem CKN.fderiv_mollify_eq_mollify_on_compact {d : ℕ} {U K : Set (Vec d)} (hU : IsOpen U) : IsCompact K → ∀ {u gi : Vec d → ℝ} {i : Fin d} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hgi : MeasureTheory.LocallyIntegrable gi MeasureTheory.volume) (hweak : HasWeakPartialDerivOn U i u gi) {ε : ℝ} (hε : 0 < ε) (hK : ∀ x ∈ K, Metric.closedBall x ε ⊆ U) {x : Vec d} (hx : x ∈ K), (fderiv ℝ (mollify u ε hε) x) (basisVec i) = mollify gi ε hε x