Theorem 3.24 — C_c^∞(ℝⁿ) is dense in W^{k,p}(ℝⁿ)

Proved

HunterPDE.Sobolev.smooth_compact_dense

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-spaces

Let $k \in \mathbb{N}$ (so $k \ge 1$ ) and $1 \le p < \infty$ . Then $C_c^\infty(\mathbb{R}^n)$ is dense in the Sobolev space $W^{k,p}(\mathbb{R}^n)$ of Definition 3.23: for every $f \in W^{k,p}(\mathbb{R}^n)$ and every $\varepsilon > 0$ there is $\varphi \in C_c^\infty(\mathbb{R}^n)$ with

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

Density lets an inequality proved for test functions (such as Theorem 3.28) be extended to all of $W^{k,p}(\mathbb{R}^n)$ , which is how Theorem 3.31 is obtained. It fails for a proper open subset $\Omega$ in place of $\mathbb{R}^n$ .

Formalization Note. The norm is sobolevNorm k p univ of Definition 3.23, valued in $[0,\infty]$ ; $\varepsilon$ ranges over positive extended reals, which is equivalent to positive reals. The notes' $\mathbb{N}$ is $\{1, 2, \dots\}$ (they write $\mathbb{N}_0 = \{0, 1, 2, \dots\}$ when $0$ is allowed, §1.8), so the statement assumes $k \ge 1$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open MeasureTheory

Formal statement

namespace HunterPDE.Sobolev

/-- Theorem 3.24 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 59: for `k ∈ ℕ` and
`1 ≤ p < ∞`, `C_c^∞(ℝⁿ)` is dense in `W^{k,p}(ℝⁿ)`: every `f ∈ W^{k,p}(ℝⁿ)` is approximated in the
norm `‖·‖_{W^{k,p}(ℝⁿ)}` of Definition 3.23 by test functions. The notes' `ℕ` is `{1, 2, …}` (they
write `ℕ₀ = {0, 1, 2, …}` when `0` is allowed, §1.8), hence `1 ≤ k`. -/
theorem smooth_compact_dense {n k : ℕ} (hk : 1 ≤ k) {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : MemW k p Set.univ f)
    (ε : ENNReal) (hε : 0 < ε) :
    ∃ φ : EuclideanSpace ℝ (Fin n) → ℝ,
      IsTestFunction Set.univ φ ∧ sobolevNorm k p Set.univ (f - φ) < ε := by sorry

end HunterPDE.Sobolev

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 59, Theorem 3.24

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting and binders. The statement quantifies over:

natural numbers $n$ and $k$ , with the hypothesis $1 \le k$ ;
an extended non-negative real $p \in [0,\infty]$ , with the hypotheses $1 \le p$ and $p \ne \infty$ , so $p \in [1,\infty)$ ;
a function $f : \mathbb{R}^n \to \mathbb{R}$ , where $\mathbb{R}^n$ is $n$ -dimensional Euclidean space with coordinates indexed by $\{0,\dots,n-1\}$ ;
the hypothesis $\mathrm{MemW}(k, p, \mathbb{R}^n, f)$ , meaning $f$ belongs to the class named MemW with parameters $k$ and $p$ on the whole space $\Omega = \mathbb{R}^n$ ;
an extended non-negative real $\varepsilon \in [0,\infty]$ , with $0 < \varepsilon$ .

Conclusion. There exists a function $\varphi : \mathbb{R}^n \to \mathbb{R}$ such that both of the following hold:

$\varphi$ $φ$ is a test function on $\mathbb{R}^n$ . By its imported definition, this means three things:
- $\varphi$ is infinitely differentiable ( $C^\infty$ ) on $\mathbb{R}^n$ ;
- $\varphi$ has compact support;
- the closed support of $\varphi$ is contained in $\Omega = \mathbb{R}^n$ . Because $\Omega$ is the whole space, this third condition always holds.
The quantity called sobolevNorm with parameters $k$ , $p$ , $\mathbb{R}^n$ , evaluated at the pointwise difference $f - \varphi$ , is strictly less than $\varepsilon$ :

\|f - \varphi\|_{k,p,\mathbb{R}^n} < \varepsilon.

What the two Sobolev-side names actually denote. These are read from the imported definitions file, not from the statement.

In the file imported by the preamble, MemW is declared with the body sorry, so its meaning is left entirely unspecified. Its declared signature there reads $\mathrm{MemW}(k, p, \Omega)$ , with $\Omega$ a set of functions on $\mathbb{R}^{k} \oplus \emptyset$ . That text has unbalanced parentheses and does not match the way the statement applies it (to $k$ , $p$ , a subset of $\mathbb{R}^n$ , and $f$ ).
No declaration named sobolevNorm appears in the imported definitions files. Its value type, and so the meaning of " $< \varepsilon$ " with $\varepsilon$ an extended non-negative real, is not fixed by any visible code.

As far as the visible code shows, both the hypothesis on $f$ and the quantity being made small are therefore opaque. Nothing in the visible code says they involve weak derivatives or $L^p$ norms.

Degenerate cases.

Target $\varepsilon = \infty$ . This value is permitted. The conclusion then only asks that sobolevNorm of $f - \varphi$ be strictly below $\infty$ .
Dimension $n = 0$ . The domain $\mathbb{R}^0$ is a single point. Every real-valued function on it is $C^\infty$ and has compact support, so the test-function condition holds for every $\varphi$ . The statement then reduces to the existence of some $\varphi$ that makes sobolevNorm of $f - \varphi$ smaller than $\varepsilon$ .
Choice $\varphi = f$ . Nothing prevents $\varphi = f$ whenever $f$ itself is a test function. In that case the difference is the zero function.
Excluded parameters. The hypotheses rule out $k = 0$ , $p < 1$ , $p = \infty$ , and $\varepsilon = 0$ ; the statement says nothing about those cases.
Vacuous hypothesis. Because MemW is unspecified (sorry), whether the hypothesis on $f$ can ever be satisfied is not determined by the visible code. If it is unsatisfiable, the statement holds vacuously.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph