Partial Differential Equations

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

Motivation

Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.

This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).

Timeline. Rellich proved the compactness of $H^1_0 \hookrightarrow L^2$ on bounded domains in 1930. Kondrachov extended it to $W^{1,p}$ and exponents below the Sobolev exponent in 1945. The $L^p$ compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of $W^{1,p}$ in 1957.

Setting

Throughout, $\mathbb{R}^n$ carries Lebesgue measure, and functions are real-valued. For an open set $\Omega \subseteq \mathbb{R}^n$, a test function $\phi \in C_c^\infty(\Omega)$ is smooth with compact support inside $\Omega$. A locally integrable $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ if $\int_\Omega g\phi = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi$ for every test function $\phi$. Here $\alpha \in \mathbb{N}_0^n$ is a multi-index of order $|\alpha| = \sum_i \alpha_i$.

For $k \in \mathbb{N}$ and $1 \le p \le \infty$, the Sobolev space $W^{k,p}(\Omega)$ consists of the $f$ whose weak derivatives $\partial^\alpha f$, $|\alpha| \le k$, exist and lie in $L^p(\Omega)$. For $p < \infty$ its norm is

$$\|f\|_{W^{k,p}(\Omega)} = \Big(\sum_{|\alpha|\le k} \int_\Omega |\partial^\alpha f|^p\,dx\Big)^{1/p},$$

and for $p = \infty$ it is the maximum of the essential suprema. The space $W^{k,p}_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in this norm. For $1 \le p < n$ the Sobolev conjugate is $p^* = np/(n-p)$.

The upper half-space is $\mathbb{R}^n_+ = \{x = (x', x_n) : x_n > 0\}$, with closure $\overline{\mathbb{R}}^n_+$ and boundary $\partial\mathbb{R}^n_+ = \{(x', 0)\} \cong \mathbb{R}^{n-1}$. The space $C_c^\infty(\overline{\mathbb{R}}^n_+)$ consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike $C_c^\infty(\mathbb{R}^n_+)$, they need not vanish on $\partial\mathbb{R}^n_+$.

A subset of a metric space is precompact if its closure is compact. $C_0(\mathbb{R}^n)$ is the space of continuous functions vanishing at infinity, with the sup norm.

In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.

Formalization targets

Goal: Rellich–Kondrachov (Theorem 3.45)

Let $\Omega$ be a bounded open set in $\mathbb{R}^n$, $1 \le p < n$ and $1 \le q < p^*$. If $\mathcal{F} \subseteq W^{1,p}_0(\Omega)$ satisfies $\|f\|_{W^{1,p}(\Omega)} \le M$ for all $f \in \mathcal{F}$, then

$$\{\, f\mathbf{1}_\Omega : f \in \mathcal{F} \,\} \ \text{is precompact in } L^q(\mathbb{R}^n).$$

Milestones

• Theorem 1.15 (Kolmogorov–Riesz). For $1 \le p < \infty$, a set $\mathcal{F} \subseteq L^p(\mathbb{R}^n)$ is precompact if and only if it is bounded, tight ($\sup_{f}\|f\|_{L^p(|x|>R)} \to 0$ as $R \to \infty$), and $L^p$-equicontinuous:

$$\forall \varepsilon > 0\ \exists \delta > 0:\ |h| < \delta \implies \|f(\cdot + h) - f\|_{L^p(\mathbb{R}^n)} < \varepsilon \quad \forall f \in \mathcal{F}.$$

• Theorem 3.41 (extension). There is a bounded linear $E : W^{1,p}(\mathbb{R}^n_+) \to W^{1,p}(\mathbb{R}^n)$ with $Ef = f$ a.e. on $\mathbb{R}^n_+$ and $\|Ef\|_{W^{1,p}(\mathbb{R}^n)} \le C(n,p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$.
• Theorem 3.42 (density). $C_c^\infty(\overline{\mathbb{R}}^n_+)$ is dense in $W^{k,p}(\mathbb{R}^n_+)$ for $1 \le p < \infty$.
• Theorem 3.44 (trace). For $1 \le p < \infty$ there is a bounded linear $T : W^{1,p}(\mathbb{R}^n_+) \to L^p(\mathbb{R}^{n-1})$ with $(Tf)(x') = f(x', 0)$ on $C_c^\infty(\overline{\mathbb{R}}^n_+)$ and $\|Tf\|_{L^p} \le C(p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$, whose kernel is exactly $W^{1,p}_0(\mathbb{R}^n_+)$.
• Theorem 3.48 ($p > n$). For $\Omega$ bounded and $n < p < \infty$, a family with $\operatorname{supp} f \Subset \Omega$ and $\|Df\|_{L^p} \le C$ is precompact in $C_0(\mathbb{R}^n)$.

The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.

Significance

The result itself. Rellich–Kondrachov is the source of compactness in the $L^2$ theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition "$u = 0$ on $\partial\Omega$" meaningful for Sobolev functions, and identifies $W^{1,p}_0$ as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.

Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal $W^{1,p}_0$ compactness theorem usable by the elliptic chapters of the same series.

Difficulty

The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of $\Omega$. The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in $L^p(\mathbb{R}^n)$. Second, the $L^q$-equicontinuity for $q$ above $p$ needs an interpolation between an $L^1$ translation estimate and the critical Sobolev embedding into $L^{p^*}$, so the Gagliardo–Nirenberg–Sobolev inequality must be available for $W^{1,p}_0(\Omega)$, not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction $q < p^*$ is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.
• Functions are ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.
• $W^{1,p}_0(\Omega)$ is the norm closure of $C_c^\infty(\Omega)$, not "zero trace". "Bounded in $W^{1,p}_0(\Omega)$" is a uniform bound on sobolevNorm 1 p Ω.
• In the goal, $\mathcal{F}$ is placed in $L^q(\mathbb{R}^n)$ by extension by zero (Ω.indicator f). The conclusion asserts both that each extension lies in $L^q$ and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis $q < p^*$ rules out $q = \infty$.
• Half-space results use dimension $n = m+1$ and the last coordinate Fin.last m. The boundary is $\mathbb{R}^m$ via $x' \mapsto (x',0)$. Extension and trace operators are maps on functions that are linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$.
• Conventions read off the page: in Theorem 3.44 the trace constant is quantified before the dimension ("depending only on $p$"), and its final clause is taken with $k = 1$ (the printed "$W^{k,p}_0$" cannot mean $k \ge 2$, as the notes remark after the proof). Theorem 3.42 is stated for $1 \le p < \infty$, and Theorem 3.41 for $1 \le p \le \infty$. Theorem 3.48 assumes $n \ge 1$.
• A trivializing reading is ruled out: the goal's conclusion is compactness of the closure in $L^q(\mathbb{R}^n)$ of the zero extensions themselves, not of some other representative. The norm bound is on the genuine weak derivatives, which the hypotheses guarantee exist, not on a junk value.
• Reusable infrastructure: weak derivatives and Sobolev spaces on open sets, the Kolmogorov–Riesz criterion, and the half-space extension and trace operators. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §1.5 and §3.9–3.10. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• H. Hanche-Olsen and H. Holden, The Kolmogorov–Riesz compactness theorem, Expositiones Mathematicae 28 (2010) 385–394. https://arxiv.org/abs/0906.4883
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §5.5–5.7. https://doi.org/10.1090/gsm/019

Motivation

Second-order elliptic equations in divergence form, such as $-\nabla\cdot(A\nabla u) + b\cdot\nabla u + cu = f$, model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space $H^1_0(\Omega)$ and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.

Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.

Setting

Let $\Omega \subseteq \mathbb{R}^n$ be open. A test function is a smooth $\phi$ with compact support in $\Omega$. The space $H^1_0(\Omega)$ is the closure of the test functions in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$; each element carries a function $u$ and a weak gradient $Du$, both square-integrable. $H^{-1}(\Omega)$ is the space of bounded linear functionals on $H^1_0(\Omega)$, and $f \in L^2(\Omega)$ acts on it by $\langle f, \phi\rangle = \int_\Omega f\phi\,dx$.

Given coefficients $a_{ij}, b_i, c \in L^\infty(\Omega)$ with $a_{ij} = a_{ji}$, the operator is

$$Lu = -\sum_{i,j=1}^n \partial_i(a_{ij}\partial_j u) + \sum_{i=1}^n \partial_i(b_i u) + cu .$$

It is uniformly elliptic if $\sum_{i,j} a_{ij}(x)\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$, almost every $x$ and every $\xi$. Its bilinear form on $H^1_0(\Omega)$ is

$$a(u,v) = \int_\Omega \Big(\sum_{i,j} a_{ij}\,\partial_i u\,\partial_j v - \sum_i b_i\,u\,\partial_i v + c\,uv\Big)dx ,$$

and the formal adjoint $L^*u = -\sum\partial_i(a_{ij}\partial_j u) - \sum b_i\partial_i u + cu$ has the form $a^*(u,v) = a(v,u)$. For $\mu \in \mathbb{R}$, $u$ is a weak solution of $Lu + \mu u = f$ with $u = 0$ on $\partial\Omega$ if $u \in H^1_0(\Omega)$ and $a(u,\phi) + \mu\int_\Omega u\phi = \langle f,\phi\rangle$ for all $\phi \in H^1_0(\Omega)$. The resolvent $K = (L+\mu I)^{-1}$ maps $f \in L^2(\Omega)$ to that solution.

A bounded operator $T$ on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is $\dim\ker T - \dim(\operatorname{ran}T)^\perp$.

Formalization targets

Goal: the Fredholm alternative (Theorem 4.24)

For $\Omega$ bounded, $L$ uniformly elliptic and $\lambda \in \mathbb{R}$, exactly one of the following holds:

$$\text{(1)}\quad \ker(L^*-\lambda) = 0 \ \text{ and } \ \forall f \in L^2(\Omega)\ \exists!\,u \in H^1_0(\Omega):\ Lu - \lambda u = f;$$ $$\text{(2)}\quad 0 < \dim\ker(L-\lambda) = \dim\ker(L^*-\lambda) < \infty,\quad Lu - \lambda u = f \text{ solvable} \iff f \perp_{L^2} \ker(L^*-\lambda),$$

with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on $H^1_0(\Omega)$.

Milestones

• Poincaré inequality (Theorem 4.9): $\int_\Omega u^2 \le C\int_\Omega |Du|^2$ on $H^1_0(\Omega)$ when $\Omega$ lies between two parallel hyperplanes. Unique solvability of $-\Delta u = f \in H^{-1}(\Omega)$ (Theorem 4.11).
• The Lax–Milgram theorem (Theorem 4.20).
• Energy estimates (Theorem 4.21): $C_1\|u\|_{H^1_0}^2 \le a(u,u) + \gamma\|u\|_{L^2}^2$ and $|a(u,v)| \le C_2\|u\|_{H^1_0}\|v\|_{H^1_0}$, with the explicit $\gamma = \theta - c_0$ if $b = 0$ and $\gamma = \tfrac{1}{2\theta}\sum\|b_i\|_{L^\infty}^2 + \tfrac\theta2 - c_0$ otherwise.
• Unique weak solvability of $Lu + \mu u = f$ for $\mu \ge \gamma$ (Theorem 4.22). The resolvent $K$ is bounded on $L^2(\Omega)$ with adjoint $(L^*+\mu I)^{-1}$, and it is compact when $\Omega$ is bounded (Theorem 4.23).
• The abstract Fredholm alternative for Fredholm operators of index zero (Theorem 4.50).
• The spectral theorem for symmetric $L$ (Theorem 4.25): eigenvalues $\lambda_1 \le \lambda_2 \le \dots \to \infty$ of finite multiplicity, with an orthonormal eigenbasis of $L^2(\Omega)$.

Significance

The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.

Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with $L^\infty$ coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.

Difficulty

The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated $\gamma$. Compactness of the resolvent needs the Rellich–Kondrachov theorem: $H^1_0(\Omega)$ embeds compactly in $L^2(\Omega)$ for bounded $\Omega$, which is not in Mathlib in this form. The goal then relates the weak problem on $H^1_0(\Omega)$ to operator statements on $L^2(\Omega)$ in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on $L^2(\Omega)$, without tracking that the solutions lie in $H^1_0(\Omega)$ and satisfy the weak identity for every $H^1_0$ test function, does not reach the stated result.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.
• $H^1_0(\Omega)$ (H10 n Ω) is modelled by jets. It is the closure, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, of the pairs $(\phi,\nabla\phi)$ for smooth compactly supported $\phi$ with support in $\Omega$. Its norm is exactly the standard $H^1$ norm, and it is a Hilbert space. $H^{-1}(\Omega)$ is StrongDual ℝ (H10 n Ω).
• Coefficients are bundled in Coeffs n. Admissible is $L^\infty(\Omega)$ membership plus a.e. symmetry. Uniform ellipticity carries $\theta > 0$.
• Weak solutions are tested against every $\phi \in H^1_0(\Omega)$, not only test functions. $f \in L^2(\Omega)$ is an element of Lp ℝ 2 on $\Omega$.
• The printed display (4.21) of the adjoint form has $+\sum b_i(\partial_i u)v$. That contradicts both $a^*(u,v) = a(v,u)$ and the stated $L^*$. The formalization uses $a^*(u,v) = a(v,u)$.
• Theorem 4.22's printed equation "$Lu + \mu f = 0$" is read as $Lu + \mu u = f$, as in Definition 4.19 and the proof.
• Theorem 4.25's printed $\lambda_1 < \lambda_2$ is stated as $\lambda_1 \le \lambda_2$, since the strict inequality fails for disconnected $\Omega$. $\Omega \neq \emptyset$ and $n \ge 1$ are assumed there.
• In Theorem 4.21 the explicit $\gamma$ is asserted for every a.e. lower bound $c_0$ of $c$, which is equivalent to the book's $c_0 = \inf c$.
• The Fredholm index is an integer computed from Module.finrank and is only used for Fredholm operators.
• Solution spaces are subspaces of $H^1_0(\Omega)$. Their finite-dimensionality is asserted separately from the equality of dimensions, so a finrank equality between two infinite-dimensional spaces (both $0$ in Lean) cannot stand in for the book's claim.
• A resolvent defined by an arbitrary choice with junk value $0$ is only used for $\mu \ge \gamma$, where the weak solution exists and is unique. The theorem asserts that this function is a continuous linear map, so it cannot be satisfied vacuously.

Needed infrastructure, reusable beyond this mission: the jet model of $H^1_0$ and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for $H^1_0(\Omega) \hookrightarrow L^2(\Omega)$, and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, Chapter 6. https://doi.org/10.1090/gsm/019
• P. D. Lax and A. N. Milgram, "Parabolic equations", Contributions to the Theory of Partial Differential Equations, Annals of Mathematics Studies 33, 1954, 167–190. https://doi.org/10.1515/9781400882182-010
• L. Gårding, "Dirichlet's problem for linear elliptic partial differential equations", Mathematica Scandinavica 1 (1953), 55–72. https://doi.org/10.7146/math.scand.a-10364
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer Classics in Mathematics, 2001, Chapter 8. https://doi.org/10.1007/978-3-642-61798-0

Motivation

Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with $k = 0$), accelerated expansion and the exterior Schwarzschild spacetime.

One headline feature of the theory is how a positive cosmological constant $\Lambda > 0$ (Assumption 2) shapes it. For $\Lambda>0$ the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For $\Lambda=0$ uniqueness fails, and for $\Lambda<0$ existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.

Setting

All FFR equations live on a single flat slice $\mathbb R^3_t$, with no time derivatives, so the formalization works on $\mathbb R^3$ with coordinates $x_1,x_2,x_3$. The spacetime metric is

$$g = (-\eta^2+|\omega|^2)\,dt^2-(\omega\otimes dt+dt\otimes\omega)+\delta_{\mathbb R^3},$$

where $\eta>0$ is the lapse and $\omega$ is a one-form on $\mathbb R^3$, identified with a vector field through the flat metric. Matter enters through the energy density $\mu$ and the momentum density $J$. Writing $\omega_{i,j}=\partial_j\omega_i$, $\nabla\cdot\omega=\omega_{i,i}$ and $\Delta$ for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are

$$2\Lambda+16\pi\mu=\frac1{\eta^2}\Big[(\nabla\cdot\omega)^2-\tfrac14\|\omega_{i,j}+\omega_{j,i}\|^2\Big],$$ $$16\pi J_i=\frac1\eta\big(\Delta\omega_i-\partial_i(\nabla\cdot\omega)\big)+\frac2{\eta^2}(\nabla\cdot\omega)\eta_i-\frac1{\eta^2}(\omega_{i,j}+\omega_{j,i})\eta_j .$$

Substituting $\omega=df+\zeta$ with $\nabla\cdot\zeta=0$ gives the elliptic form (39)–(41), with unknowns $(f,\zeta,\eta)$. Here $Q_{ij}=f_{ij}+\tfrac12(\zeta_{i,j}+\zeta_{j,i})$:

$$(\Delta f)^2-\|Q\|^2=(16\pi\mu+2\Lambda)\eta^2,$$ $$\Delta\zeta_i=16\pi J_i\eta-\tfrac2\eta(\Delta f\,\delta_{ij}-Q_{ij})\eta_j,$$ $$(\Delta f\,\delta_{ij}-Q_{ij})\eta_{ij}=8\pi\nabla\cdot(J\eta^2),$$

together with the requirement $\nabla\cdot\zeta\to0$ at infinity. Vacuum means $\mu=0$ and $J=0$. When $\Lambda>0$, the paper fixes the time orientation by the arrow-of-time convention $K=(\nabla\cdot\omega)/\eta=\Delta f/\eta>0$ (Convention 1). A pair $(\omega,\eta)$ is spherically symmetric at infinity if it is spherically symmetric on $\{r\ge r_0\}$ for some $r_0>0$. Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling $t$.

Formalization targets

Goal: Corollary 2

For $\Lambda>0$, the pair $\omega=\sqrt{\Lambda/3}\,r\,\partial_r$, $\eta=1$ is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with $\eta>0$ and $(\nabla\cdot\omega)/\eta>0$ that is spherically symmetric at infinity has the form

$$\eta\equiv c,\qquad \omega=c\sqrt{\Lambda/3}\;x\qquad(c>0).$$

Milestones

Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 ($\Lambda=0$: many vacua) and Lemma 3 ($\Lambda<0$: no vacuum).

Significance

Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with $\Lambda>0$ is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of $\Lambda$ as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the $2$-Hessian operator $\sigma_2(\nabla^2 f)$.

These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.

Difficulty

The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of $\mathbb R^3$ under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of $\Delta$) used to show $\zeta\to0$. Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on $\mathbb R^n$.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). One-forms $\omega,\zeta,J$ are vector fields $\mathbb R^3\to\mathbb R^3$, and the paper's $\omega$ is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns $0$ at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.
• "Spherically symmetric" means invariance (for scalars) or equivariance (for one-forms) under all linear isometries of $\mathbb R^3$. Because $SO(3)$ acts transitively on spheres, this is equivalent to rotational symmetry.
• The spherical symmetrization $\bar f(x)$ is the average of $f$ over the sphere of radius $|x|$, taken with respect to the surface measure volume.toSphere. "Approximately spherically symmetric at $\infty$" is read as: $f-\bar f$ is bounded and $r^2\,\|\nabla^2(f-\bar f)\|\,\|\nabla(f-\bar f)\|\to0$ uniformly as $r\to\infty$, using operator norms.
• The arrow-of-time convention $\Delta f/\eta>0$ (respectively $(\nabla\cdot\omega)/\eta>0$) is an explicit hypothesis wherever the paper invokes it. Without it, $f\mapsto-f$ (time reversal) produces a second solution.
• Existence parts are stated with explicit witnesses. A formalization that drops smoothness, $\eta>0$ or the convention would be trivial or false, and is not acceptable.
• Contributions such as maximum principles, Liouville theorems and spherical averaging in $\mathbb R^n$ are reusable well beyond this mission and are welcome as separate lemmas.

Selected references

• H. L. Bray, B. Hamm, S. Hirsch, J. Wheeler, Y. Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, 2019. https://arxiv.org/abs/1911.00967
• L. Caffarelli, L. Nirenberg, J. Spruck, The Dirichlet problem for nonlinear second order elliptic equations, III: Functions of the eigenvalues of the Hessian, Acta Mathematica 155 (1985), 261–301 (cited in the paper for the existence theory of the $J=0$ case).
• J. Corvino, R. M. Schoen, On the asymptotics for the vacuum Einstein constraint equations, Journal of Differential Geometry 73(2) (2006), 185–217 (cited in the paper for the comparison with GR).

Motivation

Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.

Setting

A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.

Formalization target

The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is

$$\exists t\geq0:\ X(t,(4,0,0))\in(-1,2)^3\quad\Longleftrightarrow\quad M\text{ halts on }w.$$

The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.

Significance and status

The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.BoxTransport.Routing.balanced_box_routing (Open).

Selected references

• OpenAI, Incompressible Box Transport and Finite Computation, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

In a short 1997 letter, Max Tegmark argued that, given the other laws of physics, a spacetime with $n$ space and $m$ time dimensions can host observers who understand and predict their world only when $(n,m)=(3,1)$ (Tegmark 1997). The argument is physical and anthropic, but each step rests on a precise mathematical fact: the classification of second-order linear PDEs into elliptic, hyperbolic and ultrahyperbolic type, the well-posedness (or ill-posedness) of the corresponding initial-value problems, the potential theory of $\mathbb R^n$, the stability of Kepler orbits, and the algebra of curvature tensors in low dimension. This mission collects those mathematical facts as formal targets.

Timeline of the ingredients cited by the letter:

• 1917 — Ehrenfest observes that planetary orbits and classical atoms are unstable when $n>3$.
• 1936 — Ásgeirsson proves his mean value theorem for the ultrahyperbolic equation.
• 1962 — Courant and Hilbert (vol. II) give the textbook treatment of PDE type and causal structure.
• 1963 — Tangherlini shows that the hydrogen atom has no bound states for $n>3$.
• 1973/1984 — Misner–Thorne–Wheeler and Deser–Jackiw–'t Hooft emphasize that general relativity has no gravitational force when $n<3$.

Setting

A second-order linear PDE on $\mathbb R^d$ has the form

$$\sum_{i,j=1}^d A_{ij}\,\partial_i\partial_j u+\sum_{i=1}^d b_i\,\partial_i u+c\,u=0,$$

with $A$ symmetric. Following the paper, at a point it is elliptic if all eigenvalues of $A$ are positive or all are negative, hyperbolic if one eigenvalue is positive and the rest negative (or vice versa), and ultrahyperbolic if at least two are positive and at least two negative. Eigenvalues are counted with multiplicity; the Lean development counts them as the positive/negative real roots of the characteristic polynomial (numPosEigenvalues, numNegEigenvalues, IsElliptic, IsHyperbolic, IsUltrahyperbolic).

A spacetime of dimensionality $(n,m)$ carries a metric $g$ with $m$ positive (time-like) and $n$ negative (space-like) eigenvalues, so that $(n,m)=(3,1)$ has signature $(+---)$. The covariant field equations $u_{;\mu}{}^{\mu}=0$ (wave) and $u_{;\mu}{}^{\mu}+\mu^2u=0$ (Klein–Gordon) have coefficient matrix $A=g^{-1}$. The Laplacian on $\mathbb R^n$ is $\nabla^2 f=\sum_i\partial_i^2 f$ (laplacian).

Formalization targets

Goal: type of the field equations as a function of $(n,m)$

For a symmetric $g$ with $m$ positive and $n$ negative eigenvalues,

$$\text{elliptic}\iff n=0\ \text{or}\ m=0,\qquad \text{hyperbolic}\iff n=1\ \text{or}\ m=1,\qquad \text{ultrahyperbolic}\iff n\ge2\ \text{and}\ m\ge2.$$

Milestones (in the order of the paper)

1. (p. L70) For $n>2$, $r^{2-n}$ is harmonic on $\mathbb R^n\setminus\{0\}$.
2. (p. L70) For $n>3$ the effective potential $U(r)=\frac{L^2}{2\mu r^2}-k\,r^{2-n}$ has no strict local minimum: no stable orbits.
3. (p. L70) For $n=3$ and $L\neq0$ it has one: stable circular orbits exist.
4. (p. L71) For $n>3$ the hydrogen energy functional is unbounded below.
5. (p. L71) For $n<3$, Ricci-flat algebraic curvature tensors in dimension $n+1$ vanish.
6. (p. L73) $g^{-1}$ has the same numbers of positive and negative eigenvalues as $g$.
7. (p. L73) The signatures $(+---)$, $(+++++)$, $(++--)$ give hyperbolic, elliptic, ultrahyperbolic equations.
8. (p. L73) The Cauchy problem for the Laplace equation with data on a line is ill-posed.
9. (p. L73) The Klein–Gordon initial-value problem is well-posed in the cones of dependence (energy estimate).
10. (p. L73) Ásgeirsson's mean value theorem for $\nabla_x^2u=\nabla_y^2u$.

Significance

The goal makes precise the paper's central new observation: the hyperbolicity needed for a well-posed initial-value problem singles out exactly one time dimension (or, in the tachyonic mirror case, one space dimension). The milestones supply the mathematical content behind each of the paper's other claims, namely instability for $n>3$ and the absence of gravity for $n<3$, as well as the well-posedness and ill-posedness facts behind the "predictability" argument. All of these are classical results; none of them is new mathematics. The value of the mission is a machine-checked record of exactly which mathematical statements the argument uses, under which hypotheses, and with which caveats (for instance the critical coupling in four dimensions).

Difficulty

The goal is linear algebra. The difficulty lies in the milestones: Ásgeirsson's theorem and the Klein–Gordon energy estimate need integration over spheres and balls, a divergence theorem or spherical-mean calculus, and differentiation under the integral sign, and Mathlib supports these only partially. The four-dimensional hydrogen case sits exactly at the Hardy-inequality threshold, where the outcome depends on the coupling constant.

Formalization scope

• Matrices are real and indexed by Fin d; eigenvalue counts are root counts of the characteristic polynomial with multiplicity. Classification is pointwise: one constant coefficient matrix.
• Functions on $\mathbb R^n$ live on EuclideanSpace ℝ (Fin n); derivatives are Fréchet derivatives, and the Laplacian is the sum of pure second derivatives along the standard basis.
• "Stable orbit" means a strict local minimum of the radial effective potential at some radius $r_0>0$.
• "No bound states" means that the energy $\int|\nabla\psi|^2-\kappa\int|x|^{2-n}\psi^2$ is unbounded below on smooth, compactly supported, $L^2$-normalized real $\psi$ (units $\hbar^2/2m=1$). For $n=4$ the claim is only asserted for $\kappa>1$, the Hardy threshold.
• "No gravity" is formalized pointwise: a tensor with the Riemann symmetries and zero Ricci contraction vanishes.
• Ill-posedness of the elliptic Cauchy problem is formalized by one explicit instance (the Laplace equation in the plane with data on $y=0$). Well-posedness of the hyperbolic one is formalized by the local energy inequality for $C^2$ Klein–Gordon solutions.

Reusable infrastructure: PDE type via eigenvalue signs, spherical means, and local energy estimates for wave-type equations.

Selected references

• M. Tegmark, On the dimensionality of spacetime, Class. Quantum Grav. 14 (1997) L69–L75. https://doi.org/10.1088/0264-9381/14/4/002
• R. Courant and D. Hilbert, Methods of Mathematical Physics, vol. II, Interscience, 1962.
• L. Ásgeirsson, Über eine Mittelwertseigenschaft von Lösungen homogener linearer partieller Differentialgleichungen 2. Ordnung mit konstanten Koeffizienten, Math. Ann. 113 (1936) 321–346.
• F. R. Tangherlini, Schwarzschild field in n dimensions and the dimensionality of space problem, Nuovo Cimento 27 (1963) 636–651.
• P. Ehrenfest, Proc. Amsterdam Acad. 20 (1917) 200.

Motivation

The free Schrödinger operator $H_0 = -\Delta$ is the Hamiltonian of a quantum particle, or of $N$ non-interacting particles, moving in $\mathbb R^n$ without external forces. Every Schrödinger operator $H = -\Delta + V$ studied in quantum mechanics is a perturbation of it, and each standard tool of the theory refers back to $H_0$: the Kato–Rellich theorem asks that $V$ be relatively bounded with respect to $H_0$, Weyl's theorem compares essential spectra with that of $H_0$, and scattering theory compares the dynamics $e^{-itH}$ with the free dynamics $e^{-itH_0}$. Knowing exactly what $H_0$ is (its domain, its self-adjointness, its spectrum and its time evolution) is therefore the base case of the spectral theory of Schrödinger operators.

All of this is obtained from one tool, the Fourier transform, which turns differentiation into multiplication. This mission follows Chapter 7 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), doi:10.1090/gsm/099. The chapter first develops the Fourier transform on the Schwartz space, on $L^1$ and on $L^2$, and then applies it to $H_0$. The same material appears in Reed–Simon (Vol. II, Sec. IX.1 and IX.7).

Setting

Write $\mathbb R^n$ for Euclidean space with $px = \sum_j p_j x_j$ and $x^2 = |x|^2$. For an integrable $f : \mathbb R^n \to \mathbb C$ the Fourier transform and its inverse are

$$\hat f(p) = \mathcal F(f)(p) = \frac{1}{(2\pi)^{n/2}}\int_{\mathbb R^n} e^{-ipx} f(x)\,d^nx, \qquad \check g(x) = \frac{1}{(2\pi)^{n/2}}\int_{\mathbb R^n} e^{ipx} g(p)\,d^np .$$

The Schwartz space $\mathcal S(\mathbb R^n)$ consists of the smooth functions all of whose derivatives decay faster than any polynomial. $L^1(\mathbb R^n)$ and $L^2(\mathbb R^n)$ are the usual Lebesgue spaces, and $C_\infty(\mathbb R^n)$ denotes the continuous functions vanishing at infinity. The convolution of $f, g \in L^1$ is $(f*g)(x) = \int f(y)g(x-y)\,d^ny$.

The Sobolev space is $H^2(\mathbb R^n) = \{\psi \in L^2 \mid p^2\hat\psi(p) \in L^2\}$. The free Schrödinger operator is

$$H_0\psi = -\Delta\psi = \mathcal F^{-1}\big(p^2\hat\psi(p)\big), \qquad \mathfrak D(H_0) = H^2(\mathbb R^n),$$

in units with $\hbar = 1$ and mass $m = 1/2$. Its time evolution is $e^{-itH_0}\psi = \mathcal F^{-1}(e^{-itp^2}\hat\psi)$. For a linear operator $A$ with domain $\mathfrak D(A)$, the resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z$ maps $\mathfrak D(A)$ bijectively onto the Hilbert space with a bounded inverse $R_A(z)$, and the spectrum is $\sigma(A) = \mathbb C\setminus\rho(A)$. For self-adjoint $A$ and a vector $\psi$, the spectral measure $\mu_\psi$ is the finite Borel measure on $\mathbb R$ with $\langle\psi, R_A(z)\psi\rangle = \int (\lambda - z)^{-1}\,d\mu_\psi(\lambda)$ for all $z \notin \mathbb R$. The absolutely continuous, singular continuous and pure point spectra $\sigma_{ac}, \sigma_{sc}, \sigma_{pp}$ are the spectra of $A$ restricted to the vectors whose spectral measures are of the respective type. A subspace $D \subseteq \mathfrak D(A)$ is a core if the closure of $A|_D$ is $A$.

Formalization targets

Goal: Theorem 7.8

For $n \ge 1$, $H_0$ is self-adjoint and

$$\sigma(H_0) = \sigma_{ac}(H_0) = [0,\infty), \qquad \sigma_{sc}(H_0) = \sigma_{pp}(H_0) = \emptyset .$$

In the Lean statement the spectral-type part is the equivalent assertion that every spectral measure $\mu_\psi$ of $H_0$ is absolutely continuous with respect to Lebesgue measure.

Milestones

• Gaussians (Lemma 7.3). For $\operatorname{Re} z > 0$, $e^{-zx^2/2} \in \mathcal S(\mathbb R^n)$ and $\mathcal F(e^{-zx^2/2})(p) = z^{-n/2} e^{-p^2/(2z)}$, with $z^{n/2} = (\sqrt z)^n$ for the principal root.
• Inversion on $\mathcal S$ (Theorem 7.4). $\mathcal F$ is a bijection of $\mathcal S(\mathbb R^n)$ with inverse $g \mapsto \check g$, and $\mathcal F^2 f(x) = f(-x)$, so $\mathcal F^4 = \mathbb I$.
• Plancherel (Theorem 7.5). $\mathcal F$ extends to a unitary operator on $L^2(\mathbb R^n)$ with $\sigma(\mathcal F) = \{1,-1,i,-i\}$.
• Riemann–Lebesgue (Lemma 7.6). $\mathcal F : L^1 \to C_\infty$ is injective and $\|\hat f\|_\infty \le (2\pi)^{-n/2}\|f\|_1$.
• Convolution (Lemma 7.7). $f * g \in L^1$, $\|f*g\|_1 \le \|f\|_1\|g\|_1$ and $(f*g)^\wedge = (2\pi)^{n/2}\hat f\hat g$.
• Core (Lemma 7.9). $C_c^\infty(\mathbb R^n)$ is a core for $H_0$.
• Asymptotics (Lemma 7.10). For $\psi \in L^2$, $e^{-itH_0}\psi(x) - (2it)^{-n/2} e^{ix^2/(4t)}\hat\psi(x/(2t)) \to 0$ in $L^2$ as $|t|\to\infty$.

Significance

The result. Theorem 7.8 says that a free quantum particle has no bound states and that its energy spectrum is purely absolutely continuous and fills $[0,\infty)$. Combined with the RAGE theorem this gives the escape of every free wave packet from bounded regions, and Lemma 7.10 makes the escape quantitative: at large times the position distribution is the momentum distribution rescaled by $2t$. The self-adjointness of $H_0$ on $H^2(\mathbb R^n)$ and the core $C_c^\infty(\mathbb R^n)$ are the inputs to the Kato–Rellich treatment of atomic Hamiltonians, and $\sigma_{ess}(H_0) = [0,\infty)$ is the reference spectrum of Weyl's theorem and of the HVZ theorem.

Formalizing it. The results are classical. Mathlib contains the Fourier transform on $L^1$, Schwartz space and $L^2$ in the normalization $e^{-2\pi i\langle x,\xi\rangle}$ (including Fourier inversion, Riemann–Lebesgue and the $L^2$ isometry), and the Prove2Me corpus holds several of these as FamousTheorems in that normalization. What is missing is Teschl's normalization with its constants, the spectrum of the $L^2$ Fourier transform, the operator $H_0$ as an unbounded self-adjoint operator, its resolvent spectrum and spectral type, and the free dynamics. This mission produces these objects in a form the later chapters (Kato–Rellich for atoms, Weyl, HVZ, scattering) can build on.

Difficulty

The Fourier-analytic milestones are close to Mathlib but not in it: every constant has to be transported from the $2\pi$-in-the-exponent convention to Teschl's $(2\pi)^{-n/2}$ convention, including the branch of $z^{n/2}$ in Lemma 7.3 and the phase $(2it)^{-n/2}$ in Lemma 7.10. The lower bound $\sigma(\mathcal F) \supseteq \{1,-1,i,-i\}$ in Theorem 7.5 needs an eigenfunction for each fourth root of unity, which the book defers to the Hermite functions of Section 8.3.

For the goal, self-adjointness and $\sigma(H_0) = [0,\infty)$ require working with the resolvent spectrum of an unbounded LinearPMap, which Mathlib does not provide, and transporting self-adjointness and resolvents through the unitary Fourier transform. The spectral-type statement requires identifying the spectral measure $\mu_\psi$ of an unbounded operator from its resolvent alone, without a spectral theorem in the library, and showing that it has a density for every $\psi \in L^2$, not only for nice $\psi$. Lemma 7.9 is a statement about the graph norm of $-\Delta$, which is not controlled by the $L^2$ norm alone.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so that $px$ and $x^2$ are the Euclidean ones, and $L^2(\mathbb R^n)$ is Lp ℂ 2 volume. fourier and fourierInv are Teschl's integrals (7.3) and (7.8) with the prefactor $(2\pi)^{-n/2}$. The $L^2$ transform $\hat\psi$ (fourierL2) is Mathlib's unitary $L^2$ transform rescaled by $\hat\psi(p) = (2\pi)^{-n/2}(\mathcal F_{\mathrm M}\psi)(p/2\pi)$, and Theorem 7.5 asserts that it is the unitary extension of (7.3). $H_0$ (freeHamiltonian) and $e^{-itH_0}$ (timeEvolution) are defined as Fourier conjugates of the maximal multiplication operator by the symbol of $-\Delta$ and of multiplication by $e^{-itp^2}$, written with Mathlib's $L^2$ transform, where the symbol is $4\pi^2|\xi|^2$. These are the same operators as Teschl's, and the domain is exactly $H^2(\mathbb R^n)$. Unbounded operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and the resolvent and spectrum are the bijective-with-bounded-inverse notions of Teschl, p. 73, not Mathlib's Banach-algebra spectrum, which is used only for the bounded operator $\mathcal F$ in Theorem 7.5. Statements that need it carry $n \ge 1$, which the book leaves implicit.

No projection-valued measure or functional calculus is taken as data. The spectral types in (7.25) are expressed through the spectral measures $\mu_\psi$, and these are pinned down intrinsically by their Borel transforms $\langle\psi, R_{H_0}(z)\psi\rangle$.

A trivializing formalization is ruled out: $\sigma(H_0)$ is the resolvent spectrum of the operator, not the essential range of $p^2$, so $\sigma(H_0) = [0,\infty)$ is not a computation on a multiplication symbol. The absolutely continuous measure in the goal must reproduce the actual resolvent matrix elements, so it cannot be chosen freely, and $e^{-itH_0}$ is not defined by its integral kernel (7.30).

A complete development needs change of normalization lemmas for the Fourier transform, the Hermite eigenfunctions of $\mathcal F$, unitary equivalence of LinearPMaps and its effect on adjoints and resolvents, self-adjointness of maximal real multiplication operators, polar coordinates on $\mathbb R^n$, and graph-norm approximation by cut-offs. The normalization bridge and the multiplication-operator results are reusable across the series. Contributions of either are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Chapter 7. https://doi.org/10.1090/gsm/099
• M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, Sections IX.1 and IX.7.
• E. M. Stein and G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Princeton University Press, 1971, Chapter I. https://doi.org/10.1515/9781400883899