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

Proved

HunterPDE.Compactness.halfSpace_density

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

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

The space $C_c^\infty(\overline{\mathbb{R}}^n_+)$ of smooth functions is dense in $W^{k,p}(\mathbb{R}^n_+)$ : for every $f \in W^{k,p}(\mathbb{R}^n_+)$ and $\varepsilon > 0$ there is $\phi \in C_c^\infty(\overline{\mathbb{R}}^n_+)$ with

\|f - \phi\|_{W^{k,p}(\mathbb{R}^n_+)} < \varepsilon.

The approximants are smooth up to the boundary but need not vanish there. This is what makes the trace map (Theorem 3.44) definable by continuity.

Formalization Note. The dimension is $n = m + 1$ , $k \in \mathbb{N}$ , and $1 \le p < \infty$ . The page gives no range of $p$ ; this is the range of the whole-space analogue, Theorem 3.24, and density fails for $p = \infty$ . $\overline{\mathbb{R}}^n_+$ is the closed half-space, not the open one.

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Compactness_Sobolev
import Definitions.Def_HunterPDE_Compactness_HalfSpace

open MeasureTheory
open scoped ENNReal

Formal statement

namespace HunterPDE.Compactness

/-- Theorem 3.42 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 72: the space `C_c^∞(ℝ̄ⁿ₊)`
of smooth functions (smooth up to the boundary, vanishing on `ℝ̄ⁿ₊` outside a compact set, not
necessarily zero on `∂ℝⁿ₊`) is dense in `W^{k,p}(ℝⁿ₊)`: every `f ∈ W^{k,p}(ℝⁿ₊)` is approximated
in the `W^{k,p}(ℝⁿ₊)` norm by such functions. Dimension `n = m + 1`, `k ∈ ℕ`, and `1 ≤ p < ∞`
(the range of the whole-space analogue, Theorem 3.24; density fails for `p = ∞`). -/
theorem halfSpace_density (m k : ℕ) (p : ℝ≥0∞) (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ) (hf : MemW k p (upperHalfSpace m) f)
    (ε : ℝ≥0∞) (hε : 0 < ε) :
    ∃ φ : EuclideanSpace ℝ (Fin (m + 1)) → ℝ, IsSmoothCompactClosedHalfSpace φ ∧
      sobolevNorm k p (upperHalfSpace m) (f - φ) < ε := by sorry

end HunterPDE.Compactness

Source

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

Read-back

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

Notation. Let $m, k \in \mathbb{N}$ , and let $p \in [1,\infty)$ : the hypotheses say $1 \le p$ and $p \ne \infty$ .

$H = \{x \in \mathbb{R}^{m+1} : x_{m+1} > 0\}$ is the open upper half-space.
$\overline{H} = \{x : x_{m+1} \ge 0\}$ is its closure.
$\mathcal{A}$ is the set of multi-indices $\alpha \in \mathbb{N}^{m+1}$ with $|\alpha| \le k$ .

Sobolev membership. " $f \in W^{k,p}(H)$ " means: for each $\alpha \in \mathcal{A}$ there is a $g \in L^p(H)$ satisfying an imported predicate "weak $\alpha$ -derivative of $f$ on $H$ ". That predicate's definition is not included.

Sobolev norm. $\|u\|_{k,p,H}$ is built from imported chosen functions $\partial^\alpha_H u$ , whose definition is not included:

\|u\|_{k,p,H} = \Bigl(\sum_{\alpha \in \mathcal{A}} \int_H |\partial^\alpha_H u|^p\,dx\Bigr)^{1/p} \in [0,\infty].

Claim. Let $f : \mathbb{R}^{m+1} \to \mathbb{R}$ with $f \in W^{k,p}(H)$ , and let $\varepsilon \in (0,\infty]$ . Then there is a function $\varphi : \mathbb{R}^{m+1} \to \mathbb{R}$ with both of these properties:

$\varphi$ is $C^\infty$ within the closed set $\overline{H}$ (differentiability relative to $\overline{H}$ at its boundary points), and there is a compact $K$ with $\varphi = 0$ on $\overline{H} \setminus K$ . Nothing is required of $\varphi$ outside $\overline{H}$ , and $\varphi$ need not vanish on $\{x_{m+1} = 0\}$ .
The pointwise difference $f - \varphi$ satisfies $\|f - \varphi\|_{k,p,H} < \varepsilon$ .

The statement does not assert $\varphi \in W^{k,p}(H)$ or $f - \varphi \in W^{k,p}(H)$ .

Degenerate cases.

$k = 0$ . $\mathcal{A} = \{0\}$ , and the norm is the $L^p(H)$ norm of the imported $\partial^0_H(f-\varphi)$ .
$m = 0$ . $H = (0,\infty) \subset \mathbb{R}$ .
$\varepsilon = \infty$ . The claim only asks for some such $\varphi$ with $\|f-\varphi\|_{k,p,H}$ finite.

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