Smooth approximation in the weak-derivative Sobolev norm

Proved

HunterPDE.Sobolev.smooth_approximation

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

approximationsobolev-spacesweak-derivatives

For every nonnegative integer $k$ , every $1\le p<\infty$ , and every $f\in W^{k,p}(\mathbb R^n)$ , a globally smooth function $g\in W^{k,p}(\mathbb R^n)$ can approximate $f$ within any positive tolerance in the norm of Definition 3.23:

\|f-g\|_{W^{k,p}(\mathbb R^n)}<\varepsilon.

This is the first step of Hunter's proof of Theorem 3.24: convolution with a standard mollifier is smooth, its weak derivatives are the convolutions of the weak derivatives of $f$ , and these converge in $L^p$ . Compact support is not required of $g$ . The order-zero case is included, and tolerances are positive extended reals.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open MeasureTheory
open HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.smooth_approximation {n k : ℕ}
    {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : MemW k p Set.univ f)
    (ε : ENNReal) (hε : 0 < ε) :
    ∃ g : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) g ∧ MemW k p Set.univ g ∧
        sobolevNorm k p Set.univ (f - g) < ε := 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, printed pp. 58–60, Definition 3.23 and proof of Theorem 3.24.

View graph