Motivation

Almost every existence theory for elliptic, parabolic and hyperbolic partial differential equations works in Sobolev spaces: function spaces defined through weak derivatives and $L^p$ integrability rather than classical differentiability. Energy methods produce solutions whose derivatives are known only to be square-integrable. Sobolev embedding theorems are what turn that information back into integrability or continuity of the solution itself, and they are used at every step of the regularity theory.

This mission covers Chapter 3, §3.1–3.8 of J. K. Hunter's graduate lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): weak derivatives, the spaces $W^{k,p}$, approximation by test functions, and the two embedding regimes $p < n$ and $p > n$.

Timeline. S. L. Sobolev proved the embedding for $p > 1$ in 1938 by potential-theoretic methods. E. Gagliardo (1958) and L. Nirenberg (1959) independently gave the elementary proof, including $p = 1$, that the notes follow. The inequality behind it, for products of functions of $n-1$ variables, is also known as the Loomis–Whitney inequality (1949). C. B. Morrey (1940) proved the Hölder estimate for $p > n$. The sharp constants were found by Federer–Fleming and Maz'ya (1960, $p = 1$, equivalent to the isoperimetric inequality) and by G. Talenti (1976, $1 < p < n$).

Setting

Throughout, $\mathbb{R}^n$ carries Lebesgue measure and the Euclidean norm $|x|$, and $\Omega \subseteq \mathbb{R}^n$ is open. A test function $\varphi \in C_c^\infty(\Omega)$ is infinitely differentiable, and its support is a compact subset of $\Omega$. For a multi-index $\alpha \in \mathbb{N}_0^n$ with $|\alpha| = \sum_i \alpha_i$, $\partial^\alpha = \partial_1^{\alpha_1}\cdots\partial_n^{\alpha_n}$.

A locally integrable $f$ has weak derivative $\partial^\alpha f = g \in L^1_{\mathrm{loc}}(\Omega)$ if

$$\int_\Omega g\,\varphi\,dx = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\varphi\,dx \quad\text{for all } \varphi\in C_c^\infty(\Omega).$$

The Sobolev space $W^{k,p}(\Omega)$, for $k\in\mathbb{N}$ and $1\le p\le\infty$, consists of the $f\in L^1_{\mathrm{loc}}(\Omega)$ whose weak derivatives $\partial^\alpha f$, $|\alpha|\le k$, exist and lie in $L^p(\Omega)$. It is normed by $\|f\|_{W^{k,p}} = \big(\sum_{|\alpha|\le k}\int_\Omega|\partial^\alpha f|^p\,dx\big)^{1/p}$, with the maximum of the suprema when $p = \infty$.

For $1\le p<n$ the Sobolev conjugate is $p^* = np/(n-p)$, so that $1/p^* = 1/p - 1/n$. For $f\in C_c^\infty(\mathbb{R}^n)$, $Df$ is the gradient, $|Df|$ its Euclidean length, and $\|Df\|_p = \big(\int|Df|^p\,dx\big)^{1/p}$. The Hölder seminorm is $[u]_{\alpha} = \sup_{x\ne y}|u(x)-u(y)|/|x-y|^\alpha$.

Formalization targets

Goal: the Gagliardo–Nirenberg–Sobolev inequality (Theorem 3.28)

For $n\ge 2$, $1\le p<n$ and every $f\in C_c^\infty(\mathbb{R}^n)$,

$$\|f\|_{p^*} \le \frac{p\,(n-1)}{2\,(n-p)}\,\|Df\|_p .$$

Milestones

1. Lemma 3.26: if $g\in L^1(\mathbb{R})$ has compact support and $\int g = 0$, then $\big|\int_{-\infty}^x g\,dt\big| \le \frac12\int|g|\,dt$.
2. Theorem 3.27, the product inequality (3.10): for nonnegative $g_i\in C_c^\infty(\mathbb{R}^{n-1})$, $\int_{\mathbb{R}^n}\prod_{i=1}^n g_i(x_i')\,dx \le \prod_{i=1}^n\|g_i\|_{n-1}$, where $x_i'$ is $x$ with the $i$th coordinate omitted.
3. Theorem 3.24: $C_c^\infty(\mathbb{R}^n)$ is dense in $W^{k,p}(\mathbb{R}^n)$ for $1\le p<\infty$.
4. Theorem 3.31: $W^{1,p}(\mathbb{R}^n)\hookrightarrow L^q(\mathbb{R}^n)$ for $1\le p<n$ and $p\le q\le p^*$, with $\|f\|_q\le C(n,p,q)\|f\|_{W^{1,p}}$.
5. Theorem 3.36 (Morrey): for $n<p<\infty$ and $\alpha = 1-n/p$ there is $C = C(n,p)$ with $[f]_\alpha\le C\|Df\|_p$ and $\sup|f|\le C\|f\|_{W^{1,p}}$ for all $f\in C_c^\infty(\mathbb{R}^n)$.

The goal's constant is explicit, and it is not the sharp one. A later sharp constant (Talenti's) would strengthen the goal but would not invalidate it.

Significance

The result. Theorem 3.28 is the quantitative core of the embedding $W^{1,p}\hookrightarrow L^{p^*}$. Density (Theorem 3.24) extends it to all of $W^{1,p}(\mathbb{R}^n)$, giving Theorem 3.31. From there, extension operators and Rellich–Kondrachov compactness follow, and with them the existence and regularity of weak solutions to elliptic equations (Chapters 4–6 of the same notes). Morrey's inequality is the complementary statement for $p>n$ and yields continuity of Sobolev functions. Without these estimates, a weak solution obtained by the Lax–Milgram or Galerkin method carries no pointwise or integrability information.

Formalizing it. Mathlib contains a Gagliardo–Nirenberg–Sobolev inequality for $C^1$ compactly supported functions with a non-explicit constant (MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, restated on the platform as FamousTheorems.gagliardo_nirenberg_sobolev and included here as a reference item). Mathlib has no weak derivatives in the integral form used here, no $W^{k,p}(\Omega)$ spaces on open sets, no density theorem for them, no $W^{1,p}\hookrightarrow L^q$ embedding, and no Morrey inequality. This mission asks for the explicit constant, the Loomis–Whitney-type product inequality in the form the proof uses, and the first results on Sobolev spaces built from integral-form weak derivatives.

Difficulty

The explicit constant cannot be read off Mathlib's existing inequality, whose constant is defined through its own proof. It has to come from the one-dimensional bound (Lemma 3.26) combined with the product inequality (3.10). Theorem 3.27 is an induction on dimension in which Hölder's inequality is applied on sections $\mathbb{R}^{n-2}$ of $\mathbb{R}^{n-1}$ and then integrated over the remaining coordinate. Expressing "$x$ with the $i$th coordinate omitted" and Fubini across those splittings of $\mathbb{R}^n$ is the bulk of the measure-theoretic bookkeeping. For $p>1$ the argument has to be applied to $|f|^s$, which is only $C^1$.

Theorems 3.24 and 3.31 need weak derivatives to commute with mollification and cutoff. They also need the weak derivative of a limit to be identified, and completeness of $L^{p^*}$. None of this is available for the integral-form definition. Morrey's inequality needs averages over balls and polar-coordinate integration.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Coordinates are 0-based (i : Fin n), and multi-indices are Fin n → ℕ. $|Df|$ is ‖gradient f x‖, which equals the operator norm of fderiv ℝ f x. $L^p$ norms are eLpNorm in $[0,\infty]$, with real exponents coerced by ENNReal.ofReal.
• $C^\infty$ is ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞). ContDiff ℝ ⊤ means analytic in current Mathlib, and using it for test functions would leave only the zero function, making every function weakly differentiable. A test function on $\Omega$ has HasCompactSupport φ and tsupport φ ⊆ Ω, so the test class is all of $C_c^\infty(\Omega)$. A smaller class would trivialize weak differentiability, and this formalization rules that out.
• Weak derivatives (Definitions 3.1, 3.2) are predicates on real functions on $\mathbb{R}^n$, of which only the values on $\Omega$ matter. MemW k p Ω f is membership in $W^{k,p}(\Omega)$. sobolevNorm is the norm of Definition 3.23, valued in $[0,\infty]$ and built from a chosen weak derivative (unique a.e.). For $p=\infty$ it uses the essential supremum.
• Constant of Theorem 3.28. The printed constant (3.11), $C(n,p) = \frac{p}{2n}\frac{n-1}{n-p}$, is false for the Euclidean $|Df|$. At $p = 1$ it equals $\frac1{2n}$, below the sharp constant $\frac1{n\alpha_n^{1/n}}$ quoted in the notes on the following page. The goal states $n\,C(n,p) = \frac{p(n-1)}{2(n-p)}$, which is what the proof's intermediate estimate $\|f\|_{p^*}\le\frac s2(\prod_i\|\partial_i f\|_p)^{1/n}$ gives.
• Theorem 3.27 writes $n = m+1$ with $m\ge1$ and states the left side as a lower Lebesgue integral of the nonnegative product. In Theorem 3.36 one constant serves (3.12) and (3.13), and the supremum bound is stated pointwise. The $p=\infty$ clause is outside the stated range and is omitted. Every existential constant is quantified after the dimension and exponents and before the function.
• Reusable beyond this mission: the weak-derivative and $W^{k,p}$ definitions (intended for the later chapters on compactness, elliptic and parabolic equations), and the product inequality. Proofs of any milestone are welcome, including ones through Mathlib's existing Sobolev-inequality machinery if they reach the explicit constant.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 3. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. Nirenberg, On elliptic partial differential equations, Ann. Scuola Norm. Sup. Pisa 13 (1959), 115–162. http://www.numdam.org/item/ASNSP_1959_3_13_2_115_0/
• E. Gagliardo, Proprietà di alcune classi di funzioni in più variabili, Ricerche Mat. 7 (1958), 102–137.
• L. H. Loomis and H. Whitney, An inequality related to the isoperimetric inequality, Bull. Amer. Math. Soc. 55 (1949), 961–962. https://doi.org/10.1090/S0002-9904-1949-09320-5
• G. Talenti, Best constant in Sobolev inequality, Ann. Mat. Pura Appl. 110 (1976), 353–372. https://doi.org/10.1007/BF02418013
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, Chapter 5. https://doi.org/10.1090/gsm/019