Theorem 3.48 — for p > n, uniform Lᵖ gradient bounds with support in Ω give precompactness in C₀(ℝⁿ)

Proved

HunterPDE.Compactness.compact_embedding_C0

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

arzela-ascolicompact-embeddingp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesobolev-spaces

Let $\Omega$ be a bounded open set in $\mathbb{R}^n$ , and $n < p < \infty$ . Suppose that $\mathcal{F}$ is a set of functions whose weak derivative belongs to $L^p(\mathbb{R}^n)$ such that: (a) $\operatorname{supp} f \Subset \Omega$ ; (b) there exists a constant $C$ such that

\|Df\|_{L^p} \le C \qquad \text{for all } f \in \mathcal{F}.

Then $\mathcal{F}$ is precompact in $C_0(\mathbb{R}^n)$ .

This is the supercritical companion of the Rellich–Kondrachov theorem. Above the dimension, gradient bounds give uniform bounds and equicontinuity, so the compactness is in the uniform norm.

Formalization Note. Each $f : \mathbb{R}^n \to \mathbb{R}$ is locally integrable, with weak first partials $\partial_i f \in L^p(\mathbb{R}^n)$ . $\operatorname{supp} f \Subset \Omega$ means that $f$ vanishes a.e. outside some compact $K \subseteq \Omega$ . $\|Df\|_{L^p}$ is the $L^p$ norm of the Euclidean length of the weak gradient, and $C$ is uniform over $\mathcal{F}$ . The conclusion states that every $f$ has a representative in Mathlib's C₀(ℝⁿ, ℝ) (a continuous representative is unique), and that the set of these representatives has compact closure in the sup norm. $n \ge 1$ is assumed, as the book's $\mathbb{R}^n$ always has it; the statement is false on $\mathbb{R}^0$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Shared_WeakDeriv

open MeasureTheory
open scoped ENNReal NNReal ZeroAtInfty

Formal statement

namespace HunterPDE.Compactness

/-- Theorem 3.48 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 75: let `Ω` be a bounded open
set in `ℝⁿ` and `n < p < ∞`. Suppose that `F` is a set of functions whose weak derivative belongs
to `Lᵖ(ℝⁿ)` such that (a) `supp f ⋐ Ω`; (b) there is a constant `C` with `‖Df‖_{Lᵖ} ≤ C` for all
`f ∈ F`. Then `F` is precompact in `C₀(ℝⁿ)`.
Each `f` is locally integrable on `ℝⁿ` with weak first partials `∂ᵢf ∈ Lᵖ(ℝⁿ)`; `supp f ⋐ Ω`
is: `f` vanishes a.e. outside a compact `K ⊆ Ω`; `‖Df‖_{Lᵖ}` is the `Lᵖ` norm of the Euclidean
length of the weak gradient. The conclusion says every `f` has a representative in `C₀(ℝⁿ)`
(continuous, vanishing at infinity; unique since continuous functions equal a.e. are equal), and
the set of these representatives has compact closure in the sup norm. `1 ≤ n` is the book's
standing `ℝⁿ` (the statement is false on `ℝ⁰`). -/
theorem compact_embedding_C0 {n : ℕ} (hn : 1 ≤ n) (Ω : Set (EuclideanSpace ℝ (Fin n)))
    (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (p : ℝ) (hnp : (n : ℝ) < p)
    (F : Set (EuclideanSpace ℝ (Fin n) → ℝ))
    (hFD : ∀ f ∈ F, ∀ i : Fin n, ∃ g : EuclideanSpace ℝ (Fin n) → ℝ,
      Shared.HasWeakDeriv Set.univ (Pi.single i 1) f g ∧ MemLp g (ENNReal.ofReal p) volume)
    (hFsupp : ∀ f ∈ F, ∃ K : Set (EuclideanSpace ℝ (Fin n)), IsCompact K ∧ K ⊆ Ω ∧
      ∀ᵐ x ∂volume, x ∉ K → f x = 0)
    (hFb : ∃ C : ℝ≥0, ∀ f ∈ F,
      eLpNorm (Shared.weakGradNorm Set.univ f) (ENNReal.ofReal p) volume ≤ (C : ℝ≥0∞)) :
    (∀ f ∈ F, ∃ u : C₀(EuclideanSpace ℝ (Fin n), ℝ), (u : EuclideanSpace ℝ (Fin n) → ℝ) =ᵐ[volume] f) ∧
      IsCompact (closure {u : C₀(EuclideanSpace ℝ (Fin n), ℝ) |
        ∃ f ∈ F, (u : EuclideanSpace ℝ (Fin n) → ℝ) =ᵐ[volume] f}) := by sorry

end HunterPDE.Compactness

Source

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

Read-back

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

Setting. Let $n \ge 1$ and let $\lambda$ be Lebesgue measure on $\mathbb{R}^n$ (Euclidean norm).

$\Omega \subseteq \mathbb{R}^n$ is open and bounded.
$p$ is a real number with $p > n$ , so $1 < p < \infty$ and the exponent used is exactly $p$ .
$F$ is a set of functions $f : \mathbb{R}^n \to \mathbb{R}$ .

Hypotheses on $F$ .

Weak derivatives in $L^p$ . For every $f \in F$ and every coordinate $i \in \{1,\dots,n\}$ there is a $g \in L^p(\mathbb{R}^n)$ satisfying an imported predicate " $g$ is a weak derivative of $f$ on $\mathbb{R}^n$ for the unit multi-index $e_i$ ". That predicate's definition is not included. $f$ itself is not assumed to lie in $L^p$ .
Support inside $\Omega$ . For every $f \in F$ there is a compact $K \subseteq \Omega$ such that, for $\lambda$ -a.e. $x$ , $x \notin K$ implies $f(x) = 0$ .
Uniform gradient bound. There is a $C \in [0,\infty)$ such that for every $f \in F$

\Bigl(\int_{\mathbb{R}^n} |G_f(x)|^p\,dx\Bigr)^{1/p} \le C,

where $G_f$ is the imported function weakGradNorm evaluated at $f$ on $\mathbb{R}^n$ . Its definition is not included; its name indicates the pointwise Euclidean length of the weak gradient.

Conclusion. Let $C_0(\mathbb{R}^n)$ be the space of continuous real functions on $\mathbb{R}^n$ tending to $0$ at infinity, with the supremum norm.

(a) Every $f \in F$ agrees $\lambda$ -a.e. with some $u \in C_0(\mathbb{R}^n)$ .
(b) Let $S = \{u \in C_0(\mathbb{R}^n) : u = f \text{ a.e. for some } f \in F\}$ . The closure of $S$ in $C_0(\mathbb{R}^n)$ , in the sup-norm topology, is compact.

Degenerate cases.

$F$ empty. $S$ is empty and both conclusions hold trivially.
$\Omega$ empty. The only compact subset of $\Omega$ is $\emptyset$ , so hypothesis 2 forces $f = 0$ a.e. Then $u = 0$ and $S \subseteq \{0\}$ .
$n = 0$ . Excluded by the hypothesis $n \ge 1$ .

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