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

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

Milestones

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

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

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

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

• 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

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)$,

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}$.