Normalized bump convolution preserves weak Sobolev membership

Proved

HunterPDE.Sobolev.memW_normed_convolution

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationconvolutionsobolev-spacesweak-derivatives

For every nonnegative derivative order $k$ , every $1\le p<\infty$ , every normalized smooth bump $\rho$ centered at zero, and every $f\in W^{k,p}(\mathbb R^n)$ ,

\rho*f\in W^{k,p}(\mathbb R^n).

This is the Sobolev membership assertion for mollification in Theorem 3.19 and the first paragraph of the proof of Theorem 3.24. It is independent of any limit of bump radii.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Mathlib.Analysis.Calculus.BumpFunction.Convolution
open MeasureTheory Filter ContinuousLinearMap
open HunterPDE.Sobolev
open scoped Convolution Topology

Formal statement

theorem HunterPDE.Sobolev.memW_normed_convolution {n k : ℕ} {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤)
    (φ : ContDiffBump (0 : EuclideanSpace ℝ (Fin n)))
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : MemW k p Set.univ f) :
    MemW k p Set.univ (φ.normed volume ⋆[lsmul ℝ ℝ, volume] f) := by sorry

Source

John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, Theorem 1.28 (printed pp. 12–13), Theorem 3.19 (printed p. 55), and proof of Theorem 3.24 (printed p. 59). Normalized shrinking smooth bumps implement the same approximate identity argument.

View graph