Theorem 3.36 — Morrey's inequality for C_c^∞(ℝⁿ), p > n

Proved

HunterPDE.Sobolev.morrey

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

holder-spacesmorrey-inequalityp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-spaces

Let $n < p < \infty$ and $\alpha = 1 - n/p$ . There is a constant $C = C(n, p)$ such that for all $f \in C_c^\infty(\mathbb{R}^n)$

[f]_\alpha \le C\, \|Df\|_p \qquad (3.12)

\sup_{\mathbb{R}^n} |f| \le C\, \|f\|_{W^{1,p}} \qquad (3.13)

where $[\cdot]_\alpha$ is the Hölder seminorm $[\cdot]_{\alpha,\mathbb{R}^n}$ of (1.1), $|Df|$ is the Euclidean length of the gradient and $\|\cdot\|_{W^{1,p}}$ is the norm of Definition 3.23.

For $p > n$ a gradient in $L^p$ forces Hölder continuity with exponent $1 - n/p$ and boundedness; this is the basis of the embedding $W^{1,p}(\mathbb{R}^n) \hookrightarrow C^{0,\alpha}(\mathbb{R}^n)$ (Theorem 3.37).

Formalization Note. One constant serves both inequalities, which is equivalent to two constants (take the larger). It is chosen after $n, p$ and before $f$ . (3.13) is stated pointwise, $|f(x)| \le C\|f\|_{W^{1,p}}$ for every $x$ , which is equivalent to the bound on the supremum. The clause "with $\alpha = 1$ if $p = \infty$ " of the printed statement is outside the stated range $n < p < \infty$ and is not formalized. Values are in $[0, \infty]$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Definitions.Def_HunterPDE_Shared_HolderSeminorm

open MeasureTheory

Formal statement

namespace HunterPDE.Sobolev

/-- Theorem 3.36 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 68 (Morrey): let `n < p < ∞`
and `α = 1 − n/p`. There is a constant `C = C(n, p)` (chosen before `f`) such that for all
`f ∈ C_c^∞(ℝⁿ)`: `[f]_α ≤ C ‖Df‖_p` (3.12), with `[·]_α` the Hölder seminorm (1.1) on `ℝⁿ` and `|Df|`
the Euclidean gradient norm, and `sup_{ℝⁿ} |f| ≤ C ‖f‖_{W^{1,p}}` (3.13), stated pointwise. -/
theorem morrey {n : ℕ} {p : ℝ} (hnp : (n : ℝ) < p) :
    ∃ C : NNReal, ∀ f : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) f → HasCompactSupport f →
        Shared.holderSeminorm (1 - (n : ℝ) / p) Set.univ f ≤
            (C : ENNReal) * eLpNorm (fun x => ‖gradient f x‖) (ENNReal.ofReal p) volume ∧
          ∀ x, ENNReal.ofReal |f x| ≤
            (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. 68, Theorem 3.36

Read-back

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

The names Shared.holderSeminorm and sobolevNorm come from imported definition files whose text is not part of this declaration.

Let $n$ be a natural number and $p$ a real number with $n < p$ . Put

\alpha = 1 - \frac{n}{p}.

Then there exists a single constant $C \ge 0$ , depending only on $n$ and $p$ and chosen before $f$ , with the following property. For every $C^\infty$ function $f : \mathbb{R}^n \to \mathbb{R}$ with compact support, both of the following hold.

(i) Hölder bound. In $[0,\infty]$ ,

\texttt{holderSeminorm}(\alpha,\,\mathbb{R}^n,\,f) \;\le\; C \cdot \big\|\,|\nabla f|\,\big\|_{L^p(\mathbb{R}^n)}.

The terms in this bound are:

$\nabla f(x)$ is the gradient of $f$ at $x$ , the vector representing the Fréchet derivative through the Euclidean inner product;
$|\nabla f(x)|$ is its Euclidean length;
$\|h\|_{L^p} = \left(\int |h|^p\,dx\right)^{1/p}$ with respect to Lebesgue measure, with $p$ passed as an extended real.

(ii) Pointwise bound. For every $x \in \mathbb{R}^n$ ,

|f(x)| \;\le\; C \cdot \texttt{sobolevNorm}(1,\,p,\,\mathbb{R}^n,\,f),

compared in $[0,\infty]$ .

Degenerate cases. For $n \ge 1$ the hypothesis forces $p > 1$ .

For $n = 0$ the hypothesis is only $p > 0$ , so $0 < p \le 1$ is permitted, and $\alpha = 1$ . In that case:

$\mathbb{R}^0$ is a single point, and every function on it is smooth with compact support;
the gradient is $0$ , so the right side of (i) is $0$ and (i) requires the Hölder seminorm to be $0$ ;
whether (i) and (ii) then hold depends on the imported definitions, which are not shown here.

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