Theorem 3.41 — bounded linear extension W^{1,p}(ℝⁿ₊) → W^{1,p}(ℝⁿ)

Proved

HunterPDE.Compactness.halfSpace_extension

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

extension-operatorp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-spaces

There is a bounded linear map $E : W^{1,p}(\mathbb{R}^n_+) \to W^{1,p}(\mathbb{R}^n)$ such that $Ef = f$ pointwise a.e. in $\mathbb{R}^n_+$ and, for some constant $C = C(n, p)$ ,

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

Extension operators let results proved on all of $\mathbb{R}^n$ (density, embeddings, compactness) be transferred to the half-space, and through local flattening to smooth domains.

Formalization Note. The dimension is $n = m + 1$ , and $p$ ranges over $1 \le p \le \infty$ (Definition 3.23's range; the page states no restriction). $E$ acts on functions $\mathbb{R}^n \to \mathbb{R}$ . It is required to be linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$ , to map it into $W^{1,p}(\mathbb{R}^n)$ , to agree with $f$ a.e. on $\mathbb{R}^n_+$ , and to obey the norm bound. $C$ and $E$ depend only on $m$ and $p$ .

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.41 of Hunter, *Notes on PDEs* (revised 6/18/2014), pp. 71–72: there is a bounded
linear map `E : W^{1,p}(ℝⁿ₊) → W^{1,p}(ℝⁿ)` such that `Ef = f` pointwise a.e. in `ℝⁿ₊` and, for
some constant `C = C(n, p)`, `‖Ef‖_{W^{1,p}(ℝⁿ)} ≤ C ‖f‖_{W^{1,p}(ℝⁿ₊)}`.
The dimension is `n = m + 1` and `1 ≤ p ≤ ∞` (the range of Definition 3.23). Functions are
`ℝⁿ → ℝ`, of which only the values on `ℝⁿ₊` matter for the input; `E` is linear up to a.e.
equality on `W^{1,p}(ℝⁿ₊)` (elements of Sobolev spaces are a.e.-classes), and `C` and `E` are
chosen after `m` and `p` only. -/
theorem halfSpace_extension (m : ℕ) (p : ℝ≥0∞) (hp : 1 ≤ p) :
    ∃ (C : ℝ≥0) (E : (EuclideanSpace ℝ (Fin (m + 1)) → ℝ) → EuclideanSpace ℝ (Fin (m + 1)) → ℝ),
      (∀ f g : EuclideanSpace ℝ (Fin (m + 1)) → ℝ,
        MemW 1 p (upperHalfSpace m) f → MemW 1 p (upperHalfSpace m) g → ∀ a b : ℝ,
          E (a • f + b • g) =ᵐ[volume] a • E f + b • E g) ∧
      ∀ f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ, MemW 1 p (upperHalfSpace m) f →
        MemW 1 p Set.univ (E f) ∧
        E f =ᵐ[volume.restrict (upperHalfSpace m)] f ∧
        sobolevNorm 1 p Set.univ (E f) ≤ (C : ℝ≥0∞) * sobolevNorm 1 p (upperHalfSpace m) f := by sorry

end HunterPDE.Compactness

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), pp. 71–72, Theorem 3.41

Read-back

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

Notation. Let $m \in \mathbb{N}$ , let $n = m+1$ , and let $p \in [1,\infty]$ ; the hypothesis is $1 \le p$ , and $p = \infty$ is allowed.

$H = \{x \in \mathbb{R}^{m+1} : x_{m+1} > 0\}$ is the open upper half-space (last coordinate positive).
$\lambda$ is Lebesgue measure on $\mathbb{R}^{m+1}$ .

Sobolev membership. For $f : \mathbb{R}^{m+1} \to \mathbb{R}$ and $\Omega \subseteq \mathbb{R}^{m+1}$ , " $f \in W^{1,p}(\Omega)$ " means the following. For each multi-index $\alpha$ of order $\le 1$ , there is a $g$ with $g \in L^p(\Omega,\lambda|_\Omega)$ satisfying an imported predicate "weak $\alpha$ -derivative of $f$ on $\Omega$ ". The multi-indices of order $\le 1$ are the zero multi-index and the unit multi-indices $e_1,\dots,e_{m+1}$ . The imported predicate's definition is not included.

Sobolev norm. $\|f\|_{1,p,\Omega} \in [0,\infty]$ is built from imported chosen functions $\partial^\alpha_\Omega f$ , whose definition is not included:

\|f\|_{1,p,\Omega} = \Bigl(\|\partial^0_\Omega f\|_{L^p(\Omega)}^p + \sum_{i=1}^{m+1} \|\partial^{e_i}_\Omega f\|_{L^p(\Omega)}^p\Bigr)^{1/p} \quad (p<\infty),

\|f\|_{1,\infty,\Omega} = \max\Bigl(\operatorname*{ess\,sup}_\Omega |\partial^0_\Omega f|,\ \max_i \operatorname*{ess\,sup}_\Omega |\partial^{e_i}_\Omega f|\Bigr) \quad (p = \infty).

Claim. There exist a constant $C \in [0,\infty)$ and a map $E$ from functions $\mathbb{R}^{m+1} \to \mathbb{R}$ to functions $\mathbb{R}^{m+1} \to \mathbb{R}$ , both depending only on $m$ and $p$ , such that:

Linearity up to null sets. For all $f, g \in W^{1,p}(H)$ and all real $a, b$ : $E(af + bg) = a\,Ef + b\,Eg$ for $\lambda$ -a.e. point of $\mathbb{R}^{m+1}$ .
The extension property. For every $f \in W^{1,p}(H)$ $f \in W^{1, p} (H)$ :
- $Ef \in W^{1,p}(\mathbb{R}^{m+1})$ (membership with $\Omega$ the whole space);
- $Ef = f$ at $\lambda$ -a.e. point of $H$ ;
- the norm bound holds:

\|Ef\|_{1,p,\mathbb{R}^{m+1}} \le C\,\|f\|_{1,p,H}.

Unconstrained points.

Nothing is said about $E$ on functions outside $W^{1,p}(H)$ .
Two inputs that agree on $H$ are not required to have the same image.
The norm bound is an inequality in $[0,\infty]$ , where $0 \cdot \infty = 0$ .

Degenerate cases. For $m = 0$ the space is $\mathbb{R}$ and $H = (0,\infty)$ . The constant $C$ is allowed to be $0$ . Whether $\|f\|_{1,p,H}$ is finite for $f \in W^{1,p}(H)$ depends on the imported chosen derivatives, which are not shown.

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