Analysis

Motivation

Chapter 9 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the differential calculus of mappings $\mathbf{f} : \mathbb{R}^n \to \mathbb{R}^m$. The definition of the derivative changes character: it is no longer a number but a linear transformation $\mathbf{f}'(\mathbf{x})$, the one that approximates the increment of $\mathbf{f}$ to first order. Once that is in place, the chapter proves the two theorems that make nonlinear analysis possible: the inverse function theorem (Theorem 9.24), which says that a continuously differentiable map with invertible derivative at a point is locally invertible with a continuously differentiable inverse, and the implicit function theorem (9.28), which solves $\mathbf{f}(\mathbf{x},\mathbf{y}) = 0$ locally for $\mathbf{x}$ in terms of $\mathbf{y}$.

The message of both is that a nonlinear map behaves locally like its linearization, provided that linearization is invertible and varies continuously.

This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the completeness and compactness results of Missions II and IV and the mean value estimates of Mission V, and it prepares the change-of-variables machinery used in Mission X.

Setting

$L(\mathbb{R}^n, \mathbb{R}^m)$ is the space of linear maps with the operator norm $\|A\| = \sup_{|x| \le 1} |Ax|$. A map $\mathbf{f}$ defined on an open $E \subseteq \mathbb{R}^n$ is differentiable at $\mathbf{x}$ with derivative $A \in L(\mathbb{R}^n,\mathbb{R}^m)$ if

$$\lim_{\mathbf{h} \to 0} \frac{|\mathbf{f}(\mathbf{x}+\mathbf{h}) - \mathbf{f}(\mathbf{x}) - A\mathbf{h}|}{|\mathbf{h}|} = 0 ,$$

and $\mathbf{f} \in \mathcal{C}'(E)$ — a $C'$-mapping — if it is differentiable on $E$ and $\mathbf{x} \mapsto \mathbf{f}'(\mathbf{x})$ is continuous. The partial derivative $D_j f_i$ is the derivative of $t \mapsto f_i(\mathbf{x} + t\mathbf{e}_j)$ at $t = 0$. A map $\varphi$ of a metric space into itself is a contraction if $d(\varphi(x),\varphi(y)) \le c\,d(x,y)$ for some $c < 1$.

Formalization targets

Goal — inverse function theorem (Theorem 9.24)

Let $\mathbf{f}$ be a $C'$-mapping of an open $E \subseteq \mathbb{R}^n$ into $\mathbb{R}^n$ and suppose $\mathbf{f}'(\mathbf{a})$ is invertible at some $\mathbf{a} \in E$. Then there are open sets $U \ni \mathbf{a}$ and $V \ni \mathbf{f}(\mathbf{a})$ such that

$$\mathbf{f}|_U \text{ is injective}, \qquad \mathbf{f}(U) = V, \qquad \mathbf{g} = (\mathbf{f}|_U)^{-1} \in \mathcal{C}'(V).$$

Milestones

$$\text{invertible operators form an open set; inversion is continuous} \qquad (9.8)$$ $$(\mathbf{g}\circ\mathbf{f})'(\mathbf{x}) = \mathbf{g}'(\mathbf{f}(\mathbf{x}))\,\mathbf{f}'(\mathbf{x}) \qquad (9.15)$$ $$\text{differentiability gives all partial derivatives} \qquad (9.17)$$ $$\|\mathbf{f}'\| \le M \text{ on a convex } E \Rightarrow |\mathbf{f}(b)-\mathbf{f}(a)| \le M|b-a| \qquad (9.19)$$ $$\mathbf{f} \in \mathcal{C}'(E) \iff \text{the } D_j f_i \text{ exist and are continuous} \qquad (9.21)$$ $$\text{a contraction of a complete metric space has a unique fixed point} \qquad (9.23)$$ $$\text{implicit function theorem} \qquad (9.28)$$ $$D_{21}f \text{ continuous at } (a,b) \Rightarrow D_{12}f(a,b) = D_{21}f(a,b) \qquad (9.41)$$ $$\text{differentiation under the integral sign} \qquad (9.42)$$

Significance

The inverse function theorem is the local classification statement of differential calculus: it says that the only local obstruction to invertibility is degeneracy of the derivative, and it is the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical criterion for the $C'$ hypothesis, since it reduces it to continuity of finitely many partial derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive, requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value theorem, whose equality form already failed in Chapter 5.

Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states the Rudin versions concretely in $\mathbb{R}^n$ — with the explicit open sets $U$ and $V$ and the inverse mapping produced as data, rather than through a bundled local homeomorphism — and so provides a bridge between the book's formulations and the library's.

Difficulty

The inverse function theorem is the first theorem in the book whose proof combines several chapters at once: the contraction principle (9.23) gives local surjectivity by solving $\mathbf{f}(\mathbf{x}) = \mathbf{y}$ as a fixed point of $\mathbf{x} \mapsto \mathbf{x} + A^{-1}(\mathbf{y} - \mathbf{f}(\mathbf{x}))$; openness of the set of invertible operators (9.8) keeps the derivative invertible near $\mathbf{a}$; the mean value inequality (9.19) controls the error; and the continuity of inversion gives the $C'$ regularity of $\mathbf{g}$. The delicate point is that all estimates must hold uniformly on a neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.

For Theorem 9.41 the trap is the hypothesis: continuity of $D_{21}f$ at the single point $(a,b)$ is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is existence of $D_{12}f$ at that point, and it genuinely fails without some such hypothesis.

Formalization scope

Conventions fixed by this mission:

• Euclidean spaces are EuclideanSpace ℝ (Fin n); linear maps are →L[ℝ] (continuous linear maps), which in finite dimension is the same as Rudin's $L(\mathbb{R}^n,\mathbb{R}^m)$, with the operator norm.
• Derivatives are HasFDerivAt, and the $C'$ condition is ContDiffOn ℝ 1.
• Partial derivatives are stated as HasDerivAt of the line restriction t ↦ f (x + t • eⱼ) at t = 0, avoiding any coordinate-projection bookkeeping; eⱼ = EuclideanSpace.single j 1.
• Invertibility of a derivative is Function.Bijective, which for a continuous linear map between finite-dimensional spaces is equivalent to the existence of a continuous linear inverse.
• In 9.8 the inverse operator is supplied as a function inv constrained on the invertible operators, so that continuity of inversion can be stated without bundling.
• Theorem 9.41 uses explicitly supplied partial derivative functions D1f, D2f, D21f, which is how Rudin states the hypotheses, and the conclusion asserts existence of D₁₂f at the point as a HasDerivAt statement.
• Theorem 9.42 is stated for the Riemann–Stieltjes integral of Mission VI, matching Rudin's hypotheses α increasing and φ(·,t) ∈ ℛ(α).

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9 (pp. 204–243).

Motivation

Brouwer's fixed point theorem says that a continuous map of a closed simplex into itself has a fixed point. Many existence questions in game theory and mathematical economics produce instead a point-to-set mapping: to each point $x$ it assigns a whole set $\Phi(x)$ of admissible responses, for instance the set of best replies of a player to the others' strategies. Such a set need not be a single point, and no continuous single-valued selection need exist. Kakutani's 1941 note, A generalization of Brouwer's fixed point theorem, gives the fixed point theorem for this setting, and shows on the same three pages that it implies two results of J. von Neumann: an intersection theorem for two closed subsets of a product of convex sets, and the minimax theorem.

Timeline, as the paper records it:

• 1912–1929: Brouwer's theorem; the paper cites the proof of Knaster, Kuratowski and Mazurkiewicz (Fund. Math. 14, 1929).
• 1928: von Neumann proves the minimax theorem for matrix games (Math. Ann. 100).
• 1937: von Neumann proves the intersection theorem (Kakutani's Theorem 2) in his paper on an economic equilibrium system, "by using a notion of integral in Euclidean spaces".
• 1941: Kakutani proves Theorem 1 (simplex), the Corollary (bounded closed convex sets), and derives Theorems 2 and 3 from it.
• 1950: Nash's existence proof for equilibrium points of $n$-person games applies Kakutani's theorem (PNAS 36).

Setting

Let $E=\mathbb R^m$ with its Euclidean norm, and let $S\subseteq E$. Kakutani writes $\mathfrak R(S)$ for the family of all closed convex subsets of $S$; as printed, it contains the empty set. A point-to-set mapping of $S$ into $\mathfrak R(S)$ assigns to each $x\in S$ a closed convex set $\Phi(x)\subseteq S$.

$\Phi$ is upper semi-continuous (in the paper's sense) when

$$x_n\in S,\quad x_n\to x_0\in S,\quad y_n\in\Phi(x_n),\quad y_n\to y_0\quad\Longrightarrow\quad y_0\in\Phi(x_0).$$

This is a sequential closed-graph condition. The paper remarks that for a closed $S$ it is equivalent to the graph $\{(x,y):x\in S,\ y\in\Phi(x)\}$ being closed in $S\times S$.

An $r$-dimensional closed simplex is the convex hull of $r+1$ affinely independent points of $E$. A fixed point of $\Phi$ is a point $x_0\in S$ with $x_0\in\Phi(x_0)$.

Formalization targets

Goal: the Corollary (p. 458)

Let $S\subseteq\mathbb R^m$ be nonempty, bounded, closed and convex, and let $\Phi$ be upper semi-continuous on $S$ with every value $\Phi(x)$, $x\in S$, a nonempty closed convex subset of $S$. Then

$$\exists\,x_0\in S:\qquad x_0\in\Phi(x_0).$$

Milestones

1. Brouwer's fixed point theorem (§1, p. 457) — a published, proved platform theorem, referenced.
2. Approximation step of the proof of Theorem 1 (pp. 457–458): for every $\varepsilon>0$ there are a point $x$ of the simplex, points $x_0,\dots,x_r$ within $\varepsilon$ of $x$, selections $y_i\in\Phi(x_i)$ and weights $\lambda\in\Delta_r$ with $x=\sum_i\lambda_ix_i=\sum_i\lambda_iy_i$.
3. Limit step of the proof of Theorem 1 (p. 458): such data for every $\varepsilon>0$, on a compact $S$, force a fixed point.
4. Theorem 1 (p. 457): the fixed point statement for an $r$-dimensional closed simplex.
5. Enclosing simplex (proof of the Corollary, p. 458): every bounded subset of $\mathbb R^m$ lies in an $m$-dimensional closed simplex $S'$.
6. Retraction (proof of the Corollary, p. 458): a continuous map of $S'$ into $S$ fixing $S$.
7. Composition (proof of the Corollary, p. 458): $x\mapsto\Phi(\psi(x))$ is upper semi-continuous on $S'$ with values in $\mathfrak R(S)\subseteq\mathfrak R(S')$.
8. Closed-graph equivalence (§1, p. 457), for closed $S$ and $\Phi(x)\subseteq S$.
9. Theorem 2 (p. 458, von Neumann's intersection theorem): if $K\subseteq\mathbb R^m$, $L\subseteq\mathbb R^n$ are bounded closed convex, $K\neq\emptyset$, and $U,V\subseteq K\times L$ are closed with all sections $U_{x_0}\subseteq L$, $V_{y_0}\subseteq K$ nonempty, closed and convex, then $U\cap V\neq\emptyset$.

Milestones 8 and 9 stand off the goal's proof path: the paper proves Theorem 2 from the Corollary, using milestone 8 to check upper semi-continuity.

Significance

The Corollary is the form in which Kakutani's theorem is used: existence of equilibrium points in $n$-person games (Nash), of competitive equilibria (Arrow–Debreu), and of solutions of generalized games and variational inequalities all reduce to a fixed point of a point-to-set mapping with nonempty closed convex values on a compact convex set. Theorem 2 in turn gives the minimax theorem (the paper's Theorem 3) in a few lines.

The results are classical and their proofs are known; what is missing is a machine-checked version. Mathlib does not contain Kakutani's theorem, and on Prove2Me the theorem is not posed. Brouwer's theorem is proved on the platform (AGT.brouwer_fixed_point) and enters as a reference milestone. Theorem 3 is already proved on the platform as a special case of Sion's minimax theorem (FamousTheorems.sion_minimax_theorem, Mathlib's Sion.minimax) and is therefore not posed here. A related open platform statement, Debreu's 1952 fixed point lemma for a contractible polyhedron with contractible values and a closed graph (SocialEquilibrium.Existence.fixed_point_of_contractible_polyhedron), generalizes Theorem 1 on polyhedra but not the Corollary, since a bounded closed convex set need not be a polyhedron. Once proved, the goal is the standard entry point for formalized equilibrium existence results.

Difficulty

Brouwer's theorem needs a continuous single-valued map, and a point-to-set mapping with closed convex values need not admit a continuous selection: the mapping on $[-1,1]$ equal to $\{1\}$ for $x<0$, $[-1,1]$ at $0$ and $\{-1\}$ for $x>0$ is upper semi-continuous and has none. So the obvious route, select and apply Brouwer, fails; any proof must pass through approximations and a limit in which the graph condition and the convexity of the limiting value both enter. The approximation step needs a family of triangulations of the simplex with mesh tending to zero, which Mathlib does not provide. The transfer from a simplex to a general convex set needs a continuous retraction, which uses convexity and closedness of $S$ in Euclidean space.

Formalization scope

• The ambient space is EuclideanSpace ℝ (Fin m), $m=0$ included. A point-to-set mapping is a total function Φ : E → Set E; only its values on $S$ are constrained.
• IsClosedConvexSubset S A is the paper's $A\in\mathfrak R(S)$ ($A\subseteq S$, closed, convex) and admits $A=\emptyset$ as printed. Nonemptiness of the values (and of $S$, and of $K$ in Theorem 2) is a separate, labelled hypothesis: with $\Phi\equiv\emptyset$, or $S=\emptyset$, the printed hypotheses hold and there is no fixed point, while the paper's proof picks "an arbitrary point $y^n$ from $\Phi(x^n)$".
• IsUpperSemicontinuous S Φ is the paper's sequential condition, with sequences in $S$ and limit $x_0\in S$. It is not Berge's open-neighbourhood upper hemicontinuity.
• Explicit readings of loose phrases: "the $n$-th barycentric simplicial subdivision" becomes "for every $\varepsilon>0$" with the selected vertices within $\varepsilon$ of the point (no subdivision is built into the statement); "it is clear that … converges" becomes compactness of $S$ in the limit step; "take a closed simplex $S'$ which contains $S$" becomes an $m$-dimensional affinely independent hull; "a continuous retracting point-to-point mapping" becomes ContinuousOn ψ S', MapsTo ψ S' S and ψ x = x on $S$; "clearly an upper semi-continuous point-to-set mapping of $S'$ into $\mathfrak R(S)\subseteq\mathfrak R(S')$" is stated as three conclusions; "closed subset of $S\times S$" is closedness in $E\times E$ (the same for closed $S$); $U\cdot V$ is $U\cap V$; "$K\times L$ in $R^{m+n}$" is the product $\mathbb R^m\times\mathbb R^n$.
• A trivializing formalization would allow empty values, an empty domain, a degenerate simplex, or approximation data for a single coarse $\varepsilon$; each is excluded by the statements as written.
• Infrastructure a complete development needs: barycentric subdivisions or another construction of approximate fixed points; nearest-point projection onto closed convex sets in Euclidean space; transport of the Corollary to $\mathbb R^m\times\mathbb R^n$ for Theorem 2. The two definitions are generic and reusable for any later set-valued existence result. Proofs by any faithful route are welcome, including a route through Brouwer's theorem and a continuous approximate selection.

Selected references

• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8 (1941), 457–459. https://doi.org/10.1215/s0012-7094-41-00838-4
• B. Knaster, C. Kuratowski, S. Mazurkiewicz, Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe, Fund. Math. 14 (1929), 132–137. https://doi.org/10.4064/fm-14-1-132-137
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Math. Ann. 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• J. von Neumann, Über ein ökonomisches Gleichungssystem und eine Verallgemeinerung des Brouwerschen Fixpunktsatzes, Ergebnisse eines Math. Kolloquiums 8 (1937), 73–83.
• J. F. Nash, Equilibrium points in n-person games, Proc. Natl. Acad. Sci. USA 36 (1950), 48–49. https://doi.org/10.1073/pnas.36.1.48
• M. Sion, On general minimax theorems, Pacific J. Math. 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.

This mission states those results for the local flow of a $C^1$ vector field on an open subset of $\mathbb{R}^n$, as in the book.

Setting

Let $M \subseteq \mathbb{R}^n$ be open and $f : M \to \mathbb{R}^n$ of class $C^1$. An integral curve of $\dot x = f(x)$ is a differentiable $\varphi$ on an open interval with $\dot\varphi(t) = f(\varphi(t))$. For each $x \in M$ there is a unique maximal one through $x$ at time $0$, defined on the open interval $I_x \ni 0$. Its value at time $t$ is $\Phi(t, x)$, the flow. The flow is local: $I_x$ may be bounded.

For $X \subseteq M$, the $\omega_+$-limit set $\omega_+(X)$ is the set of $y \in M$ for which there are $t_k \to \infty$ and $x_k \in X$ with $\Phi(t_k, x_k) \to y$. The stable and unstable sets of $\Lambda$ are $W^\pm(\Lambda) = \{x \in M : d(\Phi(t, x), \Lambda) \to 0 \text{ as } t \to \pm\infty\}$, where $d$ is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant $\Lambda$ is attracting if $W^+(\Lambda)$ is a neighborhood of $\Lambda$. A trapping region is an open connected $E$ with compact closure $\overline E \subseteq M$ such that $\Phi(t, \overline E) \subset E$ for all $t > 0$.

The divergence of $f$ is $\operatorname{div} f = \sum_i \partial f_i / \partial x_i = \operatorname{tr}(df)$. On phase space $\mathbb{R}^n \times \mathbb{R}^n \ni (p, q)$, a Hamilton function $H \in C^2$ defines Hamilton's equations $\dot q = \partial H / \partial p$, $\dot p = -\partial H / \partial q$, whose right-hand side is the Hamiltonian vector field $X_H$. The Lorenz equation is $\dot x = -\sigma(x - y)$, $\dot y = rx - y - xz$, $\dot z = xy - bz$ with $\sigma, r, b > 0$. Volume $|\cdot|$ is Lebesgue measure.

Formalization targets

Goal: Liouville's theorem (Theorem 8.10)

For $H \in C^2(\Omega)$ on an open $\Omega \subseteq \mathbb{R}^n \times \mathbb{R}^n$, with $\Phi$ the flow of $X_H$ on $\Omega$, every measurable $U \subseteq \Omega$ and every time $t$ at which all points of $U$ are alive satisfy

$$|\Phi(t, U)| = |U| .$$

Milestones

• Lemma 8.8 (Liouville's formula for volumes). Take $f \in C^1(\mathbb{R}^n)$, $U$ bounded and open, and $t_0$ with every point of $\overline U$ alive at $t_0$. Write $V(t) = |\Phi(t, U)|$. Then $V(t_0) < \infty$ and

$$\dot V(t_0) = \int_{\Phi(t_0, U)} \operatorname{div} f(x)\,dx .$$

• Theorem 8.11 (Poincaré). Let $\Phi$ be a volume preserving bijection of a bounded region $D$. Then every neighborhood $U \subseteq D$ contains an $x$ with $\Phi^k(x) \in U$ for some $k \ge 1$.
• Lemma 8.5. For a trapping region $E$, $\Lambda = \omega_+(E) = \bigcap_{t \ge 0} \Phi(t, E)$ is nonempty, invariant, compact, connected and attracting.
• Lemma 8.6. For a trapping region $E$, $W^-(x) \subseteq \omega_+(E)$ for every $x \in \omega_+(E)$.
• Lemma 8.7. For the Lorenz equation with $r \le 1$, the origin is the only fixed point, and every solution exists for all $t \ge 0$ and tends to the origin.

Significance

The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives $V(t) = V e^{-(1+\sigma+b)t}$, so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.

Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an $\omega$-limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.

Difficulty

Lemma 8.8 and Theorem 8.10 need the flow map $x \mapsto \Phi(t, x)$ to be a $C^1$ diffeomorphism of the set of points alive at time $t$ onto its image. They also need its Jacobian to satisfy the first variational equation $\dot\Pi = df(\Phi_t(x))\,\Pi$, whose determinant obeys Liouville's formula for linear systems. None of this is available for a general $C^1$ vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating $V(t)$ under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of $U$, not just $U$, to be alive at $t_0$. Without that, $\Phi(t_0, U)$ can have infinite volume ($\dot x = x^2$, $U = (0, 1)$, $t_0 = 1$).

Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about $\Phi(t, \cdot)$ must first establish that the points involved are alive at time $t$. The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function $L = rx^2 + \sigma y^2 + \sigma z^2$ from the text has $\dot L \le 0$, not $\dot L < 0$, so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points $(p, q)$, momenta first. volume on it is Lebesgue measure on $\mathbb{R}^{2n}$. The flow is a pair $(I, \Phi)$ satisfying IsMaximalFlow, which makes $t \mapsto \Phi(t, x)$ the unique maximal integral curve on $I_x$. Nothing assumes $I_x = \mathbb{R}$. The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:

• Theorem 8.10: "Hamiltonian flow" means $H \in C^2$ on an open $\Omega$. "Volume" means Lebesgue measure of any measurable $U \subseteq \Omega$ that is alive at time $t$.
• Lemma 8.8: $f \in C^1$ on $\mathbb{R}^n$. $\overline U$ is alive at $t_0$. The conclusion also states $V(t_0) < \infty$ and integrability of $\operatorname{div} f$ on $\Phi(t_0, U)$, and $V$ is the real-valued volume.
• Theorem 8.11: "region" means a measurable bounded set. "Volume preserving" means that images of measurable subsets of $D$ are measurable and have the same measure. "Any neighborhood $U$" means a neighborhood of some point, hence nonempty. $n \in \mathbb{N}$ means $k \ge 1$.
• Lemma 8.5: a trapping region has $\overline E \subseteq M$ and $\overline E$ forward complete, and "connected" includes nonempty. "Invariant" is two-sided.
• Lemma 8.7: "all solutions converge" includes existence for all $t \ge 0$. The flow is quantified universally.

A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with $\operatorname{div} X_H = 0$ assumed. It must be proved for the flow of $X_H$ built from $H$ itself.

A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula $\det \Pi(t) = \exp \int_0^t \operatorname{tr} A$ for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012 (cited: author's preliminary version, Chapter 8, pp. 229–241). https://doi.org/10.1090/gsm/140 · https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• E. N. Lorenz, Deterministic nonperiodic flow, Journal of the Atmospheric Sciences 20 (1963), 130–141. https://doi.org/10.1175/1520-0469(1963)020%3C0130:DNF%3E2.0.CO;2
• V. I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., Graduate Texts in Mathematics 60, Springer, 1989. https://doi.org/10.1007/978-1-4757-2063-1
• The Mathlib Community, Mathlib, Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4

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

Newton's law of universal gravitation states that any two point masses attract each other with a force proportional to the product of their masses and inversely proportional to the square of their distance. It is the first quantitative law of gravity (Newton, Principia, 1687) and it remains the working model of gravity in celestial mechanics, geophysics and engineering whenever relativistic effects are negligible.

The law is stated for point masses, while planets, moons and apples are extended bodies. Newton delayed publication for about twenty years because he could not prove that the Earth attracts external bodies as if all its mass were concentrated at its centre. The result that closes this gap is the shell theorem: a spherically symmetric distribution of mass exerts, on every external point, the same gravitational attraction as a point mass at its centre carrying the total mass; and mass located at radii larger than that of the test point exerts no net force at all.

Timeline (as described in the source):

• c. 1666: Newton applies the inverse-square law to the orbit of the Moon, assuming — without proof — that the Earth acts as a point mass.
• 1687: Principia published, including the proof of the shell theorem (Book I, Proposition 75, Theorem 35).
• 1798: Cavendish experiment, the first laboratory test of gravitation between masses.

Setting

Space is $\mathbb{E}^3 = \mathbb{R}^3$ with the Euclidean norm. The gravitational constant is $G = 6.67430\times10^{-11}$.

• Point force. A body of mass $m_1$ at $r_1$ exerts on a body of mass $m_2$ at $r_2$ the force

$$F_{21} = -\frac{G m_1 m_2}{\|r_{21}\|^2}\,\hat r_{21},\qquad r_{21}=r_2-r_1,\quad \hat r_{21} = \frac{r_{21}}{\|r_{21}\|}.$$

• Point field and potential. A point mass $M$ at $c$ produces the field $g(x) = -\frac{GM}{\|x-c\|^3}(x-c)$ and the potential $V(x) = -\frac{GM}{\|x-c\|}$.
• Mass distributions. An extended body is a (finite, Borel) measure $\mu$ on $\mathbb{E}^3$; $\mu(A)$ is the mass contained in the region $A$. Its gravitational field is the superposition of the point fields of its elements,

$$g_\mu(x) = \int_{\mathbb{E}^3} -\frac{G}{\|x-y\|^3}\,(x-y)\,d\mu(y).$$

• Spherical symmetry. $\mu$ is spherically symmetric (about the origin) if $\mu$ is invariant under every linear isometry of $\mathbb{E}^3$ (every rotation and reflection fixing $0$).
• Model bodies. The uniform shell $\sigma_{M,a}$ of mass $M$ and radius $a$ (normalised surface measure on the sphere $\|y\| = a$) and the uniform solid ball $\beta_{M,R}$ of mass $M$ and radius $R$ (normalised Lebesgue measure on $\|y\|<R$).

Formalization targets

Goal: shell theorem, exterior part

If $\mu$ is a finite, spherically symmetric mass distribution carried by the closed ball $\|y\|\le R$, then for every $x$ with $\|x\|>R$,

$$g_\mu(x) = -\frac{G\,\mu(\mathbb{E}^3)}{\|x\|^3}\,x .$$

Milestones

1. Vector form: $F_{12} = -F_{21}$, and $\|F_{21}\| = G m_1 m_2/\|r_2-r_1\|^2$.
2. Field form: $F_{21} = m_2\, g(r_2)$ where $g$ is the field of $m_1$ at $r_1$; the field is conservative, $g = -\nabla V$.
3. Shell theorem, interior part: mass at radii larger than $\|x\|$ exerts no net field at $x$; more precisely, the field at $x$ equals that of the mass enclosed in the ball of radius $\|x\|$, concentrated at the centre.
4. Hollow sphere: $g = 0$ inside, $g =$ point field of $M$ outside.
5. Uniform solid sphere: $g(x) = -\frac{GM}{R^3}x$ inside, point field of $M$ for $\|x\|\ge R$.

Significance

The shell theorem is what licenses treating the Sun, planets and moons as point masses in the $n$-body problem and in Kepler orbit computations, and it gives the linear growth of the gravitational field inside a uniform planet. The interior statement ("no net force inside a hollow shell") has an exact analogue in electrostatics (Coulomb's law is also inverse-square).

The results are classical and fully proved on paper. This mission asks for machine-checked proofs, together with the reusable infrastructure they require: vector-valued integrals against rotation-invariant measures, the surface measure of the sphere, and the Newtonian kernel $x/\|x\|^3$.

Difficulty

Newton's argument (or the modern one via Gauss's law) is geometric: slice the shell into rings, or apply the divergence theorem to a sphere. Neither is directly available: Mathlib has no divergence theorem on spheres in the required form, and the ring-slicing computation requires explicit spherical coordinates for a surface measure that is defined abstractly. Using symmetry alone shows the field is radial, but its magnitude requires an actual computation of a singular integral (for the interior of a solid ball the integrand is unbounded).

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). Mass distributions are Measures; the field is a Bochner integral. Because a non-integrable Bochner integral is defined to be $0$, statements where integrability is not automatic either carry an explicit integrability hypothesis or are placed where the integrand is bounded (test point strictly outside the support).
• Spherical symmetry is invariance under all linear isometries (Space ≃ₗᵢ[ℝ] Space), centred at the origin.
• Masses of model bodies are nonnegative reals (NNReal); radii are assumed strictly positive.
• The uniform shell uses Mathlib's Measure.toSphere (surface measure on the unit sphere) pushed forward by scaling.
• Units are not modelled; $G$ is the real number $6.67430\times10^{-11}$.

Contributions welcome: a general "radial field" lemma from spherical symmetry, the computation of the field of a uniform shell, and the disintegration of a spherically symmetric measure into shells.

Selected references

• Wikipedia, Newton's law of universal gravitation, revision 1370960529. https://en.wikipedia.org/w/index.php?title=Newton%27s_law_of_universal_gravitation&oldid=1370960529
• I. Newton, The Principia: Mathematical Principles of Natural Philosophy, transl. I. B. Cohen and A. Whitman, University of California Press, 1999 — Book I, Proposition 75, Theorem 35.

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