Theorem 3.31 — W^{1,p}(ℝⁿ) ↪ L^q(ℝⁿ) for p ≤ q ≤ p*

Proved

HunterPDE.Sobolev.sobolev_embedding_Lq

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

p2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-embeddingsobolev-spaces

Let $1 \le p < n$ and $p \le q \le p^*$ , where $p^* = np/(n-p)$ is the Sobolev conjugate of $p$ . Then $W^{1,p}(\mathbb{R}^n) \hookrightarrow L^q(\mathbb{R}^n)$ : there is a constant $C = C(n, p, q)$ such that every $f \in W^{1,p}(\mathbb{R}^n)$ belongs to $L^q(\mathbb{R}^n)$ and

\|f\|_q \le C\, \|f\|_{W^{1,p}} .

This is the Sobolev embedding theorem for $p < n$ on the whole space, obtained from Theorem 3.28 at $q = p^*$ by density (Theorem 3.24), and from interpolation between $L^p$ and $L^{p^*}$ for intermediate $q$ .

Formalization Note. $W^{1,p}(\mathbb{R}^n)$ and its norm are those of Definition 3.23 (MemW 1 p univ, sobolevNorm 1 p univ). The constant is a nonnegative real chosen after $n, p, q$ and before $f$ . The standing assumption $n \ge 2$ of §3.7 is implied by $1 \le p < n$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Definitions.Def_HunterPDE_Sobolev_SobolevConjugate

open MeasureTheory

Formal statement

namespace HunterPDE.Sobolev

/-- Theorem 3.31 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 66: if `1 ≤ p < n` and
`p ≤ q ≤ p*`, then `W^{1,p}(ℝⁿ) ↪ L^q(ℝⁿ)`: there is a constant `C = C(n, p, q)` such that every
`f ∈ W^{1,p}(ℝⁿ)` lies in `L^q(ℝⁿ)` with `‖f‖_q ≤ C ‖f‖_{W^{1,p}}`. The constant is chosen after
`n, p, q` and before `f`. -/
theorem sobolev_embedding_Lq {n : ℕ} {p q : ℝ} (hp : 1 ≤ p) (hpn : p < n) (hpq : p ≤ q)
    (hq : q ≤ sobolevConjugate n p) :
    ∃ C : NNReal, ∀ f : EuclideanSpace ℝ (Fin n) → ℝ,
      MemW 1 (ENNReal.ofReal p) Set.univ f →
        MemLp f (ENNReal.ofReal q) volume ∧
          eLpNorm f (ENNReal.ofReal q) volume ≤
            (C : ENNReal) * sobolevNorm 1 (ENNReal.ofReal p) Set.univ f := by sorry

end HunterPDE.Sobolev

Source

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

Read-back

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

The names sobolevConjugate, MemW and sobolevNorm come from imported definition files whose text is not part of this declaration.

Let $n$ be a natural number and $p, q$ real numbers satisfying:

$1 \le p$ ;
$p < n$ ;
$p \le q$ ;
$q \le \texttt{sobolevConjugate}(n, p)$ .

Then there exists a single constant $C \ge 0$ , depending only on $n, p, q$ and chosen before $f$ , with the following property. For every $f : \mathbb{R}^n \to \mathbb{R}$ such that MemW holds for order $1$ , exponent $p$ and the whole space $\mathbb{R}^n$ , two conclusions hold.

First, $f \in L^q(\mathbb{R}^n)$ with respect to Lebesgue measure. This means $f$ is a.e. strongly measurable and $\left(\int |f|^q\right)^{1/q} < \infty$ .

Second,

\Big(\int_{\mathbb{R}^n} |f|^q\,dx\Big)^{1/q} \;\le\; C \cdot \texttt{sobolevNorm}(1,\,p,\,\mathbb{R}^n,\,f),

compared in $[0,\infty]$ .

The exponents $p$ and $q$ are passed as extended reals via the map sending negative reals to $0$ . Since $q \ge p \ge 1$ , they are passed unchanged.

Degenerate cases. The conditions $1 \le p < n$ with $n$ a natural number force $n \ge 2$ , so $n = 0$ and $n = 1$ make the statement vacuous. Whether any $q$ exists depends on the value of sobolevConjugate, which is not shown here. If $\texttt{sobolevConjugate}(n,p) < p$ , no $q$ satisfies the hypotheses and the statement is vacuous for that $p$ .

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