Theorem 3.44 — the trace operator W^{1,p}(ℝⁿ₊) → Lᵖ(∂ℝⁿ₊) and its kernel W^{1,p}_0(ℝⁿ₊)

Proved

HunterPDE.Compactness.halfSpace_trace

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

p2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-spacestrace

For $1 \le p < \infty$ there is a bounded linear operator $T : W^{1,p}(\mathbb{R}^n_+) \to L^p(\partial\mathbb{R}^n_+)$ such that $(Tf)(x') = f(x', 0)$ for every $f \in C_c^\infty(\overline{\mathbb{R}}^n_+)$ , and

\|Tf\|_{L^p(\mathbb{R}^{n-1})} \le C \, \|f\|_{W^{1,p}(\mathbb{R}^n_+)}

for some constant $C$ depending only on $p$ . Furthermore, $f \in W^{1,p}_0(\mathbb{R}^n_+)$ if and only if $Tf = 0$ .

The trace gives boundary values to Sobolev functions, which have no pointwise values on the null set $\partial\mathbb{R}^n_+$ . It identifies $W^{1,p}_0$ as the space of functions that vanish on the boundary, which is the setting of Dirichlet problems.

Formalization Note. $n = m + 1$ , and $\partial\mathbb{R}^n_+$ is identified with $\mathbb{R}^m$ through $x' \mapsto (x', 0)$ with Lebesgue measure. $C$ is quantified before $m$ , as the page says it depends only on $p$ . The page's last sentence reads " $f \in W^{k,p}_0(\mathbb{R}^n_+)$ "; it is formalized with $k = 1$ , the space $T$ acts on, since for $k \ge 2$ the converse fails (the notes observe on p. 73 that $W^{2,p} \cap W^{1,p}_0$ is the Dirichlet condition). $T$ is linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$ , and $(Tf)(x') = f(x',0)$ holds for a.e. $x'$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Compactness_Sobolev
import Definitions.Def_HunterPDE_Compactness_HalfSpace

open MeasureTheory
open scoped ENNReal NNReal

Formal statement

namespace HunterPDE.Compactness

/-- Theorem 3.44 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 72: for `1 ≤ p < ∞` there is a
bounded linear operator `T : W^{1,p}(ℝⁿ₊) → Lᵖ(∂ℝⁿ₊)` such that `(Tf)(x′) = f(x′, 0)` for every
`f ∈ C_c^∞(ℝ̄ⁿ₊)` and `‖Tf‖_{Lᵖ(ℝⁿ⁻¹)} ≤ C ‖f‖_{W^{1,p}(ℝⁿ₊)}` for some constant `C` depending
only on `p`. Furthermore, `f ∈ W^{1,p}_0(ℝⁿ₊)` if and only if `Tf = 0`.
The dimension is `n = m + 1`, and `∂ℝⁿ₊` is identified with `ℝⁿ⁻¹ = ℝᵐ` through
`x′ ↦ (x′, 0)`; `C` is chosen before `m`, as the page says it depends only on `p`. The page's
"`f ∈ W^{k,p}_0(ℝⁿ₊)`" is read with `k = 1`, the space `T` acts on (for `k ≥ 2` the converse fails,
as the notes observe on p. 73). `T` is linear up to a.e. equality on `W^{1,p}(ℝⁿ₊)`. -/
theorem halfSpace_trace (p : ℝ≥0∞) (hp : 1 ≤ p) (hp' : p ≠ ∞) :
    ∃ C : ℝ≥0, ∀ m : ℕ, ∃ T : (EuclideanSpace ℝ (Fin (m + 1)) → ℝ) → EuclideanSpace ℝ (Fin m) → ℝ,
      (∀ f g : EuclideanSpace ℝ (Fin (m + 1)) → ℝ,
        MemW 1 p (upperHalfSpace m) f → MemW 1 p (upperHalfSpace m) g → ∀ a b : ℝ,
          T (a • f + b • g) =ᵐ[volume] a • T f + b • T g) ∧
      (∀ f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ, MemW 1 p (upperHalfSpace m) f →
        MemLp (T f) p volume ∧
          eLpNorm (T f) p volume ≤ (C : ℝ≥0∞) * sobolevNorm 1 p (upperHalfSpace m) f) ∧
      (∀ f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ, IsSmoothCompactClosedHalfSpace f →
        T f =ᵐ[volume] fun x' => f (boundaryPoint x')) ∧
      (∀ f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ, MemW 1 p (upperHalfSpace m) f →
        (MemW0 1 p (upperHalfSpace m) f ↔ T f =ᵐ[volume] 0)) := by sorry

end HunterPDE.Compactness

Source

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

Read-back

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

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

$H_m = \{x \in \mathbb{R}^{m+1} : x_{m+1} > 0\}$ is the open upper half-space and $\overline{H}_m$ its closure $\{x_{m+1} \ge 0\}$ .
$\lambda_m$ is Lebesgue measure on $\mathbb{R}^m$ .
For $x' \in \mathbb{R}^m$ , $(x',0) \in \mathbb{R}^{m+1}$ is $x'$ with $0$ appended as the last coordinate.

Sobolev membership. " $f \in W^{1,p}(H_m)$ " means: for the zero multi-index and each unit multi-index $e_i$ , there is a $g \in L^p(H_m)$ satisfying an imported predicate "weak derivative of $f$ on $H_m$ ". That predicate's definition is not included.

Sobolev norm. $\|f\|_{1,p,H_m}$ is built from imported chosen functions $\partial^\alpha f$ , whose definition is not included:

\|f\|_{1,p,H_m} = \Bigl(\int_{H_m} |\partial^0 f|^p + \sum_{i=1}^{m+1} \int_{H_m} |\partial^{e_i} f|^p\Bigr)^{1/p}.

$W^{1,p}_0$ membership. " $f \in W^{1,p}_0(H_m)$ " means both of the following:

$f \in W^{1,p}(H_m)$ ;
for every $\varepsilon \in (0,\infty]$ there is a $\varphi$ satisfying an imported predicate "test function on $H_m$ " with $\|f - \varphi\|_{1,p,H_m} < \varepsilon$ . That predicate's definition is not included.

Claim. There is one constant $C \in [0,\infty)$ , the same for every dimension, such that for every $m \in \mathbb{N}$ there is a map $T$ from functions $\mathbb{R}^{m+1} \to \mathbb{R}$ to functions $\mathbb{R}^m \to \mathbb{R}$ with the following four properties:

Linearity up to null sets. For all $f, g \in W^{1,p}(H_m)$ and real $a, b$ : $T(af+bg) = a\,Tf + b\,Tg$ at $\lambda_m$ -a.e. point.
Boundedness. For every $f \in W^{1,p}(H_m)$ : $Tf \in L^p(\mathbb{R}^m)$ and

\Bigl(\int_{\mathbb{R}^m} |Tf|^p\,d\lambda_m\Bigr)^{1/p} \le C\,\|f\|_{1,p,H_m}.

Agreement with boundary values. For every $f$ that is $C^\infty$ within $\overline{H}_m$ and vanishes on $\overline{H}_m$ outside some compact set (with no membership in $W^{1,p}(H_m)$ assumed): $(Tf)(x') = f(x',0)$ for $\lambda_m$ -a.e. $x'$ .
Characterisation of $W^{1,p}_0$ . For every $f \in W^{1,p}(H_m)$ : $f \in W^{1,p}_0(H_m)$ if and only if $Tf = 0$ $\lambda_m$ -a.e.

Unconstrained points.

Nothing is said about $T$ on other inputs.
Inputs agreeing on $H_m$ are not required to have the same image.

Degenerate cases.

$m = 0$ . $\mathbb{R}^0$ is a single point carrying unit mass. "Almost everywhere" then means "at that point", and the $L^p$ norm of $Tf$ is $|Tf(\text{pt})|$ . Property 3 reads $Tf(\text{pt}) = f(0)$ for such $f$ on $[0,\infty)$ . Property 4 says $f \in W^{1,p}_0((0,\infty))$ iff $Tf(\text{pt}) = 0$ .
$C = 0$ . The constant is allowed to be $0$ .
$\varepsilon = \infty$ . In the $W^{1,p}_0$ definition, $\varepsilon = \infty$ is permitted.

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