Analysis

Motivation

Long-time behaviour is the central question about an autonomous differential equation $\dot x = f(x)$: where does a trajectory go as $t \to \pm\infty$? In the plane this question has an almost complete answer. The theory begun by Poincaré (Mémoire sur les courbes définies par une équation différentielle, 1881–1886) and completed by Bendixson (Sur les courbes définies par des équations différentielles, Acta Math. 24, 1901, doi:10.1007/BF02403068) shows that a bounded planar trajectory can only accumulate on equilibria, on a periodic orbit, or on a chain of equilibria joined by connecting orbits. Chaotic behaviour, which already occurs for three-dimensional flows such as the Lorenz system, is excluded. It is the standard tool for proving that a planar system has a limit cycle, and it underlies Hilbert's 16th problem.

This mission formalizes Section 7.3 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS Graduate Studies in Mathematics 140, 2012), pp. 220–224, which proves the classical theorem and the generalized version with finitely many fixed points.

Setting

Let $M \subseteq \mathbb{R}^2$ be open and $f \in C^1(M, \mathbb{R}^2)$. An integral curve at $x$ is a function $\varphi$ on an open interval $J \ni 0$ with $\varphi(0) = x$, $\varphi(J) \subseteq M$ and $\dot\varphi(s) = f(\varphi(s))$ on $J$. The union of all such $J$ is the maximal interval $I_x = (T_-(x), T_+(x))$. The flow $\Phi(t, x)$, $t \in I_x$, is the value at time $t$ of the maximal integral curve at $x$. With $\sigma \in \{+,-\}$:

• the orbit is $\gamma(x) = \{\Phi(t,x) : t \in I_x\}$, and the half-orbit $\gamma_\sigma(x)$ keeps only $t \in I_x$ with $\sigma t > 0$;
• a fixed point is a point with $f(x) = 0$; a periodic point is a point with $\Phi(T, x) = x$ for some $T > 0$ in $I_x$ (fixed points included). A regular periodic orbit is the orbit of a periodic point that is not fixed, and a non-closed orbit is the orbit of a point that is not periodic;
• the $\omega_\sigma$-limit set $\omega_\sigma(x)$ is the set of $y \in M$ with $\Phi(t_k, x) \to y$ for some times $t_k \in I_x$, $t_k \to \sigma\infty$;
• a set $U \subseteq M$ is $\sigma$ invariant if $\gamma_\sigma(x) \subseteq U$ for every $x \in U$;
• a transversal arc $\Sigma = s(J)$ is the image of a $C^1$ embedding $s$ of an open interval $J$ into $M$ with $\dot s \ne 0$ and $\dot s_1 f_2(s) - \dot s_2 f_1(s) \neq 0$ on $J$. The parameter orders the points of $\Sigma$.

In Lean, points are Fin 2 → ℝ (general Fin n → ℝ for the Chapter 6 notions), and $\sigma$ is a Bool with true for $+$. The definitions are lifetime, flow, orbit, halfOrbit, omegaLimitSet, IsPeriodicPoint and IsTransversalArc, all in the namespace TeschlODE.Planar.

Formalization targets

Goal: the generalized Poincaré–Bendixson theorem (Theorem 7.16)

Fix $x \in M$ and $\sigma$, and suppose $\omega_\sigma(x) \neq \emptyset$ is compact, connected and contains only finitely many fixed points. Then one of three cases holds:

$$\text{(i) } \omega_\sigma(x) = \{x_0\},\ f(x_0) = 0; \qquad \text{(ii) } \omega_\sigma(x) = \gamma(y),\ y \text{ periodic},\ f(y) \neq 0;$$ $$\text{(iii) every } y \in \omega_\sigma(x) \text{ with } f(y) \ne 0 \text{ lies on a non-closed orbit } \gamma(y) \subseteq \omega_\sigma(x) \text{ with } \omega_+(y) = \{a\},\ \omega_-(y) = \{b\},$$

where $a, b$ are fixed points in $\omega_\sigma(x)$.

Milestones

1. Lemma 7.9. The successive intersections of $\gamma_\sigma(x_0)$ with a transversal arc through a regular point $x_0$ are monotone along the arc.
2. Corollary 7.10. $\omega_\sigma(x)$ meets a transversal arc in at most one point.
3. Corollary 7.11. If $\omega_\sigma(x) \cap \gamma_\sigma(x) \neq \emptyset$, then $x$ is periodic and $\omega_+(x) = \omega_-(x) = \gamma(x)$.
4. Corollary 7.12. A minimal compact $\sigma$ invariant set is a periodic orbit.
5. Lemma 7.13 (Poincaré–Bendixson). A nonempty compact $\omega_\sigma(x)$ without fixed points is a regular periodic orbit.
6. Lemma 7.14. A connected $\omega_\sigma(x)$ that contains a regular periodic orbit $\gamma(y)$ equals $\gamma(y)$.
7. Lemma 7.15. If $\omega_\sigma(x)$ is compact, at most one orbit in $\omega_\sigma(x)$ runs from a fixed point $x_-$ to a distinct fixed point $x_+$.

Significance

The theorem turns the existence of periodic solutions into a topological statement. It is enough to find a compact positively invariant region with no equilibria, often an annulus bounded by two curves on which the vector field points inward. This is how periodic orbits are established for the van der Pol and Liénard equations (Theorem 7.8 of the same chapter) and for many models in biology and chemistry. The generalized version also describes limit sets that contain equilibria, such as homoclinic and heteroclinic cycles. Corollary 7.12 records the dimensional boundary: in the plane every minimal set is a periodic orbit, while from dimension three on minimal sets can be invariant tori with dense orbits.

The results have been proved for over a century. None of them is formalized in Mathlib or on the platform. Mathlib has omegaLimit for global flows on topological spaces and existence and uniqueness of integral curves, but no local flow of a vector field on an open set, no transversal sections and no Jordan curve theorem. This mission produces a machine-checked planar limit-set theory. The local flow and limit-set layer it needs is reusable for every later chapter on dynamical systems.

Difficulty

The statements are topological, and the proofs rest on the Jordan curve theorem for piecewise $C^1$ curves: a closed curve made of an orbit segment and a piece of transversal arc separates the plane, and trajectories cannot cross it in the forbidden direction. That theorem is not in Mathlib, and the platform's Jordan-curve and Schoenflies statements are open. Everything that looks one-dimensional in a sketch, "the orbit enters the inside and is trapped", depends on it. The ingredients a sketch treats as obvious also need care: the flow-box straightening (Lemma 6.2), the local return map to a transversal arc (Lemma 6.9), and the invariance, closedness and connectedness of limit sets (Lemmas 6.5–6.6). Generic arguments about compact invariant sets do not suffice: the conclusions are false in $\mathbb{R}^3$, so any proof must use planarity.

Formalization scope

• Points are Fin 2 → ℝ. Its sup norm induces the Euclidean topology, and no statement depends on the norm. $f$ is a total function with ContDiffOn ℝ 1 f M on the open set $M$.
• The flow is defined, not assumed. lifetime f M x is the union of domains of integral curves at $x$, and flow f M t x is the value at $t$ of such a curve, selected by choice (unique for $C^1$ fields). Outside $I_x$ the flow has the junk value $x$, and no statement evaluates it there. Limit points must lie in $M$, as in the book.
• $\sigma \in \{\pm\}$ is a Bool; true means $+$ (atTop), false means $-$ (atBot).
• "Periodic" includes fixed points (period zero), as in the book. "Regular periodic" is periodic with $f(y) \neq 0$, and "non-closed" is not periodic.
• A transversal arc is a $C^1$ topological embedding of an open interval into $M$. The book says "smooth", so these statements cover a wider class of arcs and are at least as strong as the book's. Lemma 7.9's "monotone sequence of intersections" is stated as: any parametrization $u$ of the intersection points ($s(u(t)) = \Phi(t, x_0)$) is monotone or antitone on the set of intersection times.
• "Connected" is IsPreconnected; nonemptiness is a separate hypothesis. "Finitely many fixed points" is Set.Finite {y ∈ ω_σ(x) | f y = 0}. The book's "$\omega_\pm(y) \in \{x_j\}$" is $\omega_\pm(y) = \{a\}$ for a fixed point $a \in \omega_\sigma(x)$. No statement uses O(·), "sufficiently small" or an unspecified constant.
• The four hypotheses on $\omega_\sigma(x)$ (nonempty, compact, connected, finitely many fixed points) are the book's and are all kept. A formalization that drops one of them, or reads "regular periodic orbit" to include a fixed point, is not the theorem.
• Needed infrastructure: local existence, uniqueness and continuity of the flow (Chapter 2, 6.1), the flow box, the Jordan curve theorem for piecewise $C^1$ curves, and the basic limit-set lemmas of Chapter 6. Contributions of any of these as separate lemmas are welcome, and the Jordan curve theorem in particular is reusable far beyond this mission.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012 (author's preliminary version, §7.3). doi:10.1090/gsm/140, author's copy
• I. Bendixson, Sur les courbes définies par des équations différentielles, Acta Mathematica 24 (1901), 1–88. doi:10.1007/BF02403068
• M. W. Hirsch, S. Smale, R. L. Devaney, Differential Equations, Dynamical Systems, and an Introduction to Chaos, 3rd ed., Academic Press, 2013, Ch. 10. doi:10.1016/C2009-0-61160-0
• L. Perko, Differential Equations and Dynamical Systems, 3rd ed., Springer, 2001, §3.7. doi:10.1007/978-1-4613-0003-8

Motivation

Most differential equations that model physical, biological or engineered systems cannot be solved in closed form, yet the question asked about them is usually qualitative: does the system settle down to an equilibrium, and does it stay near the equilibrium when perturbed? Liapunov's direct method answers that question without solving the equation, by exhibiting a function that does not increase along solutions. It is the standard tool of nonlinear stability analysis and of control design, where a controller is typically certified by a Liapunov function for the closed-loop system (Khalil, Nonlinear Systems).

A Liapunov function whose values strictly decrease along every non-constant solution gives asymptotic stability directly. In practice the natural candidate, often the total energy of a damped mechanical system, only satisfies a non-strict inequality. The Krasovskii–LaSalle invariance principle closes that gap: if the function is not constant along any complete orbit other than the equilibrium, the equilibrium is still asymptotically stable. It was established by Barbashin and Krasovskii (1952) and by LaSalle (1960, IRE Trans. Circuit Theory 7).

This mission formalizes Chapter 6 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version), from the local flow of an autonomous equation, through limit sets, to the principle itself.

Setting

Fix $n \in \mathbb{N}$, an open set $M \subseteq \mathbb{R}^n$ (the phase space) and a vector field $f : M \to \mathbb{R}^n$ of class $C^1$. The autonomous system is $\dot x = f(x)$. An integral curve is a differentiable map $\varphi$ from an open interval $J$ into $M$ with $\dot\varphi(t) = f(\varphi(t))$ for all $t \in J$.

For each $x \in M$ there is a maximal interval $I_x = (T_-(x), T_+(x)) \ni 0$ and a unique maximal integral curve $t \mapsto \Phi(t, x)$ on $I_x$ with $\Phi(0, x) = x$: every integral curve through $x$ at time $0$ is a restriction of it. The map $\Phi$ on $W = \{(t, x) : x \in M,\ t \in I_x\}$ is the flow. It is a local flow: $I_x$ may be bounded, because solutions can leave $M$ or blow up in finite time.

The orbit of $x$ is $\gamma(x) = \{\Phi(t, x) : t \in I_x\}$ and the forward orbit is $\gamma_+(x) = \{\Phi(t, x) : t \in I_x,\ t > 0\}$ ($\gamma_-(x)$ with $t < 0$). The $\omega_+$-limit set $\omega_+(x)$ is the set of $y \in M$ with $\Phi(t_k, x) \to y$ for some times $t_k \to +\infty$ in $I_x$; $\omega_-(x)$ uses $t_k \to -\infty$.

A point $x_0 \in M$ with $f(x_0) = 0$ is a fixed point. It is stable if every neighborhood $U'$ of $x_0$ contains a neighborhood $V$ of $x_0$ such that solutions starting in $V$ exist and stay in $U'$ for all $t \ge 0$. It is asymptotically stable if moreover $\Phi(t, x) \to x_0$ as $t \to \infty$ for all $x$ in some neighborhood of $x_0$.

A Liapunov function at $x_0$ is a continuous $L : U \to \mathbb{R}$ on an open neighborhood $U \subseteq M$ of $x_0$ with $L(x_0) = 0$, $L > 0$ on $U \setminus \{x_0\}$, and $L(\varphi(t_0)) \ge L(\varphi(t_1))$ for every integral curve $\varphi$ and all $t_0 < t_1$ with $\varphi(t_0), \varphi(t_1) \in U \setminus \{x_0\}$. It is strict if the inequality is always strict. $S_\delta$ denotes the connected component of $\{x \in U : L(x) \le \delta\}$ containing $x_0$.

Formalization targets

Goal: Theorem 6.14 (Krasovskii–LaSalle principle)

Let $x_0$ be a fixed point and $L$ a Liapunov function at $x_0$ on $U$. Write $(\ast)$ for: $L$ is not constant on any orbit lying entirely in $U \setminus \{x_0\}$, i.e. every $y \in M$ with $\gamma(y) \subseteq U \setminus \{x_0\}$ has points $a, b \in \gamma(y)$ with $L(a) \ne L(b)$. Then

$$(\ast) \ \Longrightarrow\ x_0 \text{ is asymptotically stable}; \qquad L \text{ strict} \ \Longrightarrow\ (\ast);$$

and, under $(\ast)$, every $x \in M$ whose forward orbit lies in a compact subset of $U$ satisfies $\Phi(t, x) \to x_0$ as $t \to \infty$.

Milestones

In attack order: Theorem 6.1 (the maximal flow exists, $W$ is open, $\Phi$ is $C^k$ on $W$, and $\Phi(t+s, x) = \Phi(t, \Phi(s, x))$); Lemma 6.3 (a forward orbit in a compact subset of $M$ forces $T_+(x) = \infty$); Lemma 6.6 ($\omega_\pm(x)$ is then nonempty, compact and connected); Lemma 6.7 ($d(\Phi(t, x), \omega_\pm(x)) \to 0$); Theorem 6.15 (a function non-increasing along $\gamma_+(x) \subseteq U$ is constant on $\omega_+(x) \cap U$); Lemma 6.11 (a closed $S_\delta$ is positively invariant); Lemma 6.12 ($S_\varepsilon \subseteq B_\delta(x_0)$ and $B_\varepsilon(x_0) \subseteq S_\delta$); Theorem 6.13 (Liapunov: a Liapunov function makes $x_0$ stable).

Significance

The result itself. The invariance principle is the form of Liapunov's method used in applications. It gives asymptotic stability of damped mechanical systems from their energy, of gradient systems from their potential, and of adaptive and passivity-based controllers, where the natural Liapunov function is only non-increasing. Its limit-set formulation (Theorem 6.15) is also the entry point to the Poincaré–Bendixson theory of the next chapter, which uses the same $\omega$-limit sets.

Formalizing it. Mathlib has local existence and uniqueness for ODEs and a theory of $\omega$-limit sets for global flows (omegaLimit, Flow). It has no maximal solution of an ODE, no local flow with its maximal intervals, and no Liapunov stability theory. The results are classical and proved in the book; none has a machine-checked proof on this platform. This mission builds the local-flow and limit-set layer and the Liapunov layer on top of it.

Difficulty

The central difficulty is that the flow is local. The book's arguments pass freely between "the solution stays in a compact set" and "the solution exists for all positive time" (Lemma 6.3). In a formal setting every statement about $\Phi(t, x)$ must first establish $t \in I_x$, and the maximal interval must be constructed from local solutions. Theorem 6.1 on its own requires gluing local solutions into a maximal one and proving that the domain $W$ is open with $C^k$ dependence on initial conditions.

A common first idea is to assume the vector field is complete, so that Mathlib's global Flow and omegaLimit apply directly. That assumption is not available: the goal concerns orbits that stay in the neighborhood $U$, and completeness of such orbits is a consequence of the argument, not a hypothesis. Similarly, $L$ is only continuous, so a derivative-based criterion $\nabla L \cdot f \le 0$ cannot replace condition (6.36).

Formalization scope

The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm, and $B_r(x_0)$ is the open ball Metric.ball. The standing assumption $f \in C^k(M, \mathbb{R}^n)$, $k \ge 1$, $M$ open, is a binder of every theorem (as ContDiffOn ℝ 1 f M, the weakest case, and for general $k \ge 1$ in Theorem 6.1). The flow enters as a pair (I, Φ) satisfying IsMaximalFlow f M I Φ, which characterizes the maximal integral curves uniquely. Theorem 6.1 proves that such a pair exists, so no completeness or extra regularity is assumed. The two time directions $\sigma \in \{\pm\}$ of Lemmas 6.3–6.7 are one statement with a real parameter σ = 1 ∨ σ = -1. The $\omega$-limit set contains only points of $M$, as in the book.

Stability conclusions include existence of the solution for all $t \ge 0$. The Liapunov condition quantifies over every integral curve and constrains only the two endpoint values, exactly as (6.36). $L$ is a total function whose values off $U$ are never read.

Correction to the printed statement. The book's final sentence of Theorem 6.14, "every orbit lying entirely in $U(x_0)$ converges to $x_0$", is false as printed. With $U = M = \mathbb{R}^2$ and a strict Liapunov function, some orbits escape to infinity (Khalil, §4.1). The goal therefore asks for convergence of every forward orbit contained in a compact subset of $U$, which is what the book's argument uses. The other two parts are as printed.

A trivializing formalization is ruled out: stability and asymptotic stability are stated for the maximal flow, with existence for all $t \ge 0$ required, and not for an arbitrary map Φ or a flow assumed global. Asymptotic stability keeps both conjuncts, stability and attraction.

Needed infrastructure: maximal solutions of $C^1$ autonomous ODEs and their continuation (reusable across Chapters 6–13), openness of $W$ and smooth dependence on initial data, compactness arguments for limit sets, and connected components of sublevel sets. Contributions of the local-flow layer as standalone lemmas are especially welcome, since later missions of this series rely on the same objects.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012; author's preliminary version, Chapter 6, pp. 187–208. https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf (published book: https://doi.org/10.1090/gsm/140)
• J. P. LaSalle, Some extensions of Liapunov's second method, IRE Transactions on Circuit Theory 7 (1960), 520–527. https://doi.org/10.1109/TCT.1960.1086720
• E. A. Barbashin and N. N. Krasovskii, On global stability of motion, Doklady Akademii Nauk SSSR 86 (1952), 453–456.
• H. K. Khalil, Nonlinear Systems, 3rd ed., Prentice Hall, 2002, §4.1–4.2. https://www.pearson.com/en-us/subject-catalog/p/nonlinear-systems/P200000003359

Why initial value problems come first

Almost every quantitative statement about an ordinary differential equation, from the stability of an equilibrium to the existence of a periodic orbit, presupposes that the equation has a solution through each initial point and, usually, that this solution is unique and depends continuously on the data. Chapter 2 of Gerald Teschl's graduate textbook Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) establishes these facts for first-order systems in $\mathbb{R}^n$. It is the foundation for the rest of the series: the flows, limit sets, Poincaré maps and invariant manifolds of later chapters are all built on the existence, uniqueness and extension results proved here.

A short history. Local existence was first proved in the nineteenth century by polygonal approximation (Cauchy) under differentiability-type hypotheses. Lipschitz isolated the condition that bears his name. Picard and Lindelöf established existence and uniqueness by successive approximation, and Banach (1922) abstracted the argument into the contraction principle. Peano (1890) showed that continuity of the right-hand side alone suffices for existence, without uniqueness. Gronwall's inequality and its integral generalisations give the continuous dependence estimates. Teschl's chapter presents all of these in a uniform notation.

Setting

An initial value problem (IVP) is

$$\dot x = f(t, x), \qquad x(t_0) = x_0, \qquad (2.10)$$

where $f$ is a continuous map from an open set $U \subseteq \mathbb{R} \times \mathbb{R}^n$ to $\mathbb{R}^n$ and $(t_0, x_0) \in U$. Here $|x|$ is the Euclidean norm on $\mathbb{R}^n$. A solution on an interval $I$ is a function $x : I \to \mathbb{R}^n$ whose graph $\{(t, x(t)) : t \in I\}$ lies in $U$ and which is differentiable on $I$ (one-sidedly at an endpoint that belongs to $I$) with $\dot x(t) = f(t, x(t))$. Such a solution is automatically continuously differentiable.

The function $f$ is locally Lipschitz in the second argument, uniformly with respect to the first, if for every compact $V_0 \subseteq U$ there is a constant $L$ with $|f(t,x) - f(t,y)| \le L|x - y|$ whenever $(t,x), (t,y) \in V_0$ (the book's (2.18)).

For $T, \delta > 0$ let $V = [t_0, t_0 + T] \times \bar B_\delta(x_0)$, where $\bar B_\delta(x_0) = \{x : |x - x_0| \le \delta\}$, let $M = \max_V |f|$, and define the existence time

$$T_0 = \min\Bigl\{T, \frac{\delta}{M}\Bigr\}, \qquad \text{with } \frac{\delta}{M} = \infty \text{ when } M = 0 .$$

The chapter also works in a real Banach space $X$, a complete normed real vector space, where a contraction of a closed set $C \subseteq X$ is a map $K : C \to C$ with $\|K(x) - K(y)\| \le \theta\|x - y\|$ for some $\theta \in [0, 1)$.

Formalization targets

Goal: Peano's existence theorem (Theorem 2.19)

If $f$ is continuous on $V = [t_0, t_0 + T] \times \bar B_\delta(x_0)$ and $M = \max_V |f|$, then there is a function $x$ with $x(t_0) = x_0$ solving

$$\dot x(t) = f(t, x(t)), \qquad |x(t) - x_0| \le \delta, \qquad t \in [t_0, t_0 + T_0],$$

and the analogous statement holds on $[t_0 - T_0, t_0]$ with $V = [t_0 - T, t_0] \times \bar B_\delta(x_0)$. No Lipschitz condition is assumed and the solution need not be unique.

Milestones

1. Theorem 2.1 (contraction principle). A contraction of a nonempty closed subset of a Banach space has a unique fixed point $\bar x$, and $\|K^m(x) - \bar x\| \le \frac{\theta^m}{1-\theta}\|K(x) - x\|$ for every $x \in C$.
2. Theorem 2.2 (Picard–Lindelöf). Under the local Lipschitz condition, (2.10) has a solution on an open interval around $t_0$; two solutions on any interval containing $t_0$ coincide; and a solution exists on $[t_0, t_0 + T_0]$ with graph in $V$ (and on $[t_0 - T_0, t_0]$).
3. Theorem 2.4 (Weissinger). If $\|K^m(x) - K^m(y)\| \le \theta_m\|x - y\|$ with $\sum \theta_m < \infty$, then $K$ has a unique fixed point and $\|K^m(x) - \bar x\| \le \bigl(\sum_{j \ge m}\theta_j\bigr)\|K(x) - x\|$.
4. Lemma 2.7 (generalised Gronwall). $\psi \le \alpha + \int_0^t \beta\psi$ with $\beta \ge 0$ implies $\psi(t) \le \alpha(t) + \int_0^t \alpha(s)\beta(s)e^{\int_s^t \beta}\,ds$, and $\psi(t) \le \alpha(t)e^{\int_0^t\beta}$ for nondecreasing $\alpha$.
5. Theorem 2.8 (continuous dependence). $|x(t) - y(t)| \le |x_0 - y_0|e^{L|t-t_0|} + \frac{M}{L}(e^{L|t-t_0|} - 1)$ for solutions of $\dot x = f(t,x)$ and $\dot y = g(t,y)$.
6. Theorem 2.17 (global existence). If $|f(t,x)| \le M(T) + L(T)|x|$ on $[-T, T] \times \mathbb{R}^n$ for every $T > 0$, every solution extends to all of $\mathbb{R}$.
7. Theorem 2.18 (Arzelà–Ascoli). A bounded, equicontinuous sequence in $C([a,b], \mathbb{R}^n)$ has a uniformly convergent subsequence.

Significance

Peano's theorem is the existence statement with the weakest regularity hypothesis on $f$ in the classical theory. It is what lets one speak of solutions of equations with non-Lipschitz right-hand sides, such as $\dot x = \sqrt{|x|}$, and it is the starting point for the theory of non-unique solutions and differential inclusions. The explicit existence time $T_0 = \min\{T, \delta/M\}$ is the quantitative form used whenever one needs a uniform lower bound on the lifetime of solutions starting in a compact set. Picard–Lindelöf, Gronwall and continuous dependence together make the IVP well posed. The global existence theorem under linear growth is used throughout the later chapters to define global flows.

Mathlib already contains a Picard–Lindelöf theorem (IsPicardLindelof), Gronwall's inequality in differential form, the Banach fixed point theorem for complete (extended) metric spaces, and an Arzelà–Ascoli theorem for bounded continuous functions. It does not contain Peano's theorem, the integral form of the generalised Gronwall inequality with variable $\alpha$, Weissinger's theorem, or global existence under linear growth. The statements here are phrased in the book's setting: one-sided intervals, the $M = 0$ convention for $T_0$, local Lipschitz conditions on an open set, $\mathbb{R}^n$-valued functions. Connecting them to the existing Mathlib results is part of the work.

Difficulty

For Peano's theorem the obvious approach, Picard iteration, does not apply. Without a Lipschitz condition the integral operator $x \mapsto x_0 + \int_{t_0}^t f(s, x(s))\,ds$ need not be a contraction on any ball, its fixed points need not be unique, and a sequence of approximate solutions need not converge. Any argument has to produce a solution without a uniqueness mechanism and still reach the full interval $[t_0, t_0 + T_0]$ that the theorem specifies, not merely some shorter one. On the formal side, derivatives relative to closed intervals, the $M = 0$ corner of $T_0$, and passing between the differential and the integral form of the IVP all need care.

For Theorem 2.17 the difficulty is that "every solution is defined on all of $\mathbb{R}$" is a statement about maximal solutions, and the book defines these only through a gluing construction. Without a Lipschitz condition that construction is no longer unique. An a-priori bound on $|x(t)|$ alone does not give extension beyond a finite endpoint.

Formalization scope

• State space. $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm. The right-hand side is a total function $f : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^n$; hypotheses restrict attention to $U$ or $V$. Banach spaces are real normed spaces with CompleteSpace.
• Solutions. IsSolutionOn U f I x: for every $t \in I$, $(t, x(t)) \in U$ and $x$ has derivative $f(t, x(t))$ at $t$ relative to $I$. Initial conditions are separate hypotheses.
• Closed ball. The book writes the open ball $B_\delta(x_0)$ in Theorems 2.2 and 2.19 but takes a maximum over $V$ and uses $|x(t) - x_0| \le \delta$ in the proofs. The statements use the closed ball: over the open ball the maximum may not exist, and the solution can reach the sphere at $t_0 + T_0$.
• Quantifier readings. "The maximum of $|f|$ on $V$" is a variable $M$ with IsGreatest {|f(p)| : p ∈ V} M. $T_0$ is if M = 0 then T else min T (δ / M). "Some interval around $t_0$" in Theorem 2.2 is $\exists \varepsilon > 0$ with $(t_0 - \varepsilon, t_0 + \varepsilon)$, and "unique" means uniqueness on every interval containing $t_0$. In Theorem 2.8 the suprema $L$, $M$ of (2.41) become arbitrary constants $L \ge 0$, $M$ bounding the same quantities, which is equivalent because the bound is monotone in both; the case $L = 0$ uses the limit $M|t - t_0|$. In Theorem 2.17 the constants $M(T), L(T)$ are existential inside $\forall T > 0$, so they may depend on $T$ but not on $x$. "All solutions are defined for all $t$" means that every solution on an open interval extends to a solution on $\mathbb{R}$.
• Hypotheses of Theorem 2.17. Section 2.6 opens with a standing assumption of local uniqueness, but Theorem 2.17's own text needs only continuity and (2.66), and the book's remark after Theorem 2.13 covers maximal solutions without uniqueness. The statement assumes only continuity of $f$ and (2.66); it is therefore at least as strong as the book's.
• Added regularity. Lemma 2.7 assumes $\psi, \alpha, \beta$ continuous on $[0, T]$, which the book leaves implicit.
• Ruling out trivial readings. An existence statement in which the interval collapses to a point would be trivially true. Here $T, \delta > 0$ are required, $T_0 = T$ when $M = 0$ (never Lean's $\delta/0 = 0$), and a solution must satisfy the differential equation at every point of $[t_0, t_0 + T_0]$ with the book's $T_0$, not on some unspecified shorter interval.

A complete development needs derivatives within intervals, interval integrals, uniform convergence and compactness in $C([a,b], \mathbb{R}^n)$. The definitions IsSolutionOn and LocallyLipschitzSecond are reused throughout the Teschl series. Contributions that connect these statements to Mathlib's IsPicardLindelof, ContractingWith and BoundedContinuousFunction.arzela_ascoli are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, American Mathematical Society, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf ; published version: https://doi.org/10.1090/gsm/140
• G. Peano, Démonstration de l'intégrabilité des équations différentielles ordinaires, Mathematische Annalen 37 (1890), 182–228. https://doi.org/10.1007/BF01200235
• S. Banach, Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales, Fundamenta Mathematicae 3 (1922), 133–181. https://doi.org/10.4064/fm-3-1-133-181

Motivation

In one complex variable the Riemann mapping theorem classifies a whole class of domains by topology alone: every nonempty simply connected proper subdomain of $\mathbb{C}$ is biholomorphic to the unit disc. Nothing of the kind holds in several variables. The two most obvious generalizations of the disc to $\mathbb{C}^n$, the unit ball and the unit polydisc, are homeomorphic, yet no biholomorphic map carries one onto the other. This is the first result a student of several complex variables meets that has no one-variable shadow, and it is the standard illustration that the geometry of the boundary, not the topology of the domain, governs holomorphic equivalence.

As recounted in the source, Poincaré (1907) observed the inequivalence by computing the automorphism groups of $\mathbb{D}^2$ and $\mathbb{B}_2$, assuming the maps extend past the boundary; H. Cartan gave the first complete proof in 1931; and Rothstein (1935) proved that there is not even a proper holomorphic map from the bidisc to the ball. This mission follows the presentation in §1.4–1.6 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026), where the inequivalence is derived from a general theorem on proper maps out of product domains, followed by Cartan's uniqueness theorem and the basic structure theory of zero sets and injective maps.

Setting

Write $\mathbb{C}^n$ for $n$-tuples $z = (z_1, \dots, z_n)$ of complex numbers, $\mathbb{D} = \{\zeta \in \mathbb{C} : |\zeta| < 1\}$ for the unit disc, and $\|z\| = (|z_1|^2 + \cdots + |z_n|^2)^{1/2}$ for the Euclidean norm. The unit ball and unit polydisc are

$$\mathbb{B}_n = \{ z \in \mathbb{C}^n : |z_1|^2 + \cdots + |z_n|^2 < 1 \}, \qquad \mathbb{D}^n = \{ z \in \mathbb{C}^n : |z_k| < 1 \text{ for } k = 1, \dots, n \},$$

and the unit sphere is $S^{2n-1} = \partial\mathbb{B}_n = \{ z : |z_1|^2 + \cdots + |z_n|^2 = 1 \}$. A domain is a nonempty connected open set. A map between open subsets of complex spaces is holomorphic if it is complex differentiable at every point.

A continuous map $f : U \to V$ is proper if $f^{-1}(K)$ is compact for every compact $K \subset V$. A biholomorphic map $f : U \to V$ is a holomorphic bijection whose inverse is holomorphic; every biholomorphism is proper. An analytic disc is a nonconstant holomorphic map $\varphi : \mathbb{D} \to \mathbb{C}^n$, and a set $S$ contains no analytic discs if no analytic disc has $\varphi(\mathbb{D}) \subset S$. A circular domain is a domain $U$ with $e^{i\theta} z \in U$ whenever $z \in U$ and $\theta \in \mathbb{R}$.

Formalization targets

Goal: Rothstein's theorem (Theorem 1.4.4)

$$\text{there is no proper holomorphic map } f : \mathbb{D}^2 \to \mathbb{B}_2 .$$

The path to the goal

• Proposition 1.4.6. $S^{2n-1}$ contains no analytic discs.
• Lemma 1.4.7. For bounded domains $U \subset \mathbb{R}^n$, $V \subset \mathbb{R}^m$ and continuous $f : U \to V$: $f$ is proper if and only if, whenever $p_k \in U$ and $p_k \to p \in \partial U$, every limit point of $\{f(p_k)\}$ lies in $\partial V$.
• Theorem 1.4.8. If $U = U' \times U'' \subset \mathbb{C}^n \times \mathbb{C}^k$ ($n, k \ge 1$) and $V \subset \mathbb{C}^m$ are bounded domains and $\partial V$ contains no analytic discs, there is no proper holomorphic map $U \to V$.

Further results on the same definitions

• Theorem 1.5.1 (Cartan). If $U \subset \mathbb{C}^n$ is a bounded domain, $a \in U$, $f : U \to U$ holomorphic, $f(a) = a$ and $Df(a) = I$, then $f(z) = z$ on $U$.
• Corollary 1.5.2. A biholomorphism $f : U \to V$ of bounded circular domains with $f(0) = 0$ is the restriction of a linear map.
• Theorem 1.6.1 (Riemann extension). If $g \in \mathcal{O}(U)$ is not identically zero on a domain $U$ and $f \in \mathcal{O}(U \setminus g^{-1}(0))$ is locally bounded in $U$, then $f$ extends uniquely to some $F \in \mathcal{O}(U)$.
• Theorem 1.6.2. The zero set of a holomorphic function that is not identically zero on a domain is, on an open dense subset of itself, locally a graph $z_n = g(z_1, \dots, z_{n-1})$ after reordering the variables.
• Theorem 1.6.6. An injective holomorphic map $U \to \mathbb{C}^n$ on an open $U \subset \mathbb{C}^n$ has nowhere vanishing Jacobian determinant; a holomorphic bijection between open sets of $\mathbb{C}^n$ is biholomorphic.

The goal is chosen as the textbook's headline result of §1.4. Theorem 1.4.8 is strictly more general; it is a milestone, so a solver may prove the goal as its special case.

Significance

Rothstein's theorem implies the biholomorphic inequivalence of $\mathbb{B}_2$ and $\mathbb{D}^2$, the basic example that the Riemann mapping theorem has no analogue in several variables. Theorem 1.4.8 isolates the reason: a boundary that contains analytic discs cannot be mapped properly into a boundary that contains none. Cartan's uniqueness theorem and its corollary are the standard tools for computing automorphism groups of the ball and the polydisc. The Riemann extension theorem, the local graph structure of zero sets and the Jacobian criterion for injective maps are used throughout the theory of analytic varieties and of holomorphic mappings.

All of these results are classical and proved in the source. None of them is formalized in Mathlib or on the platform for $\mathbb{C}^n$ with $n \ge 2$: Mathlib has one-variable Riemann removable singularities and the maximum modulus principle, and the platform has one-variable results on injective holomorphic maps. This mission produces machine-checked statements of the several-variable versions, and infrastructure (proper maps between subsets, analytic discs, holomorphic families) that later chapters of the series reuse.

Difficulty

The goal cannot be reached through topology: $\mathbb{D}^2$ and $\mathbb{B}_2$ are homeomorphic, so any argument must use holomorphy essentially and must see the boundary. The step that needs genuine analysis is passing from properness, a statement about compact sets, to a statement about boundary values of holomorphic functions of one variable along slices of the product domain; this requires normal families (Montel's theorem) in several variables, which Mathlib does not provide in the needed form. Cartan's theorem rests on power-series expansions in homogeneous parts and vector-valued Cauchy estimates on polydiscs. Theorem 1.6.2 needs the holomorphic implicit function theorem and Rouché's theorem, and Theorem 1.6.6 an induction on dimension that runs through Theorem 1.6.2. The Riemann extension theorem needs holomorphy of parameter-dependent Cauchy integrals.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ. Mathlib's norm on this type is the sup norm, so Metric.ball 0 1 is the polydisc, not the ball. The ball and the sphere are therefore defined with the explicit Euclidean condition, unitBall n = {z | ∑ k, ‖z k‖ ^ 2 < 1} and unitSphere n = {z | ∑ k, ‖z k‖ ^ 2 = 1}. The polydisc is written coordinatewise as unitPolydisc n. Reading the ball as the sup-norm ball would trivialize the goal (the identity of the bidisc is a proper holomorphic self-map); the definitions exclude that reading. Boundedness is Bornology.IsBounded, and boundaries are Mathlib's frontier; neither depends on the norm. A domain is IsOpen U ∧ IsConnected U, so it is nonempty.

Holomorphic means DifferentiableOn ℂ on an open set. On open sets this is equivalent to the book's Definition 1.1.2 (Proposition 1.1.3 and Theorem 1.2.1). Maps into $\mathbb{C}^m$ are Fin m → ℂ-valued. $Df(a)$ is fderiv ℂ f a, and the Jacobian determinant is LinearMap.det of it. Maps are ambient functions whose values off the relevant set are irrelevant. Consequently:

• Proper is IsProperMapOn f U V: f maps U into V, is continuous on U, and U ∩ f ⁻¹' K is compact for every compact K ⊆ V. This is Definition 1.4.3 for the restricted map. It is not IsProperMap of the ambient map.
• Uniqueness in Theorem 1.6.1 is uniqueness on $U$.
• The inverse of a biholomorphism is a function g holomorphic on $V$ with Set.InvOn g f U V.

Lemma 1.4.7 works in Fin n → ℝ and reads "limit point of the sequence $\{f(p_k)\}$" as a cluster point of the sequence (MapClusterPt). Theorem 1.4.8 uses the product type (Fin n → ℂ) × (Fin k → ℂ) for $\mathbb{C}^n \times \mathbb{C}^k$. In Theorem 1.6.2, "after reordering the variables" means choosing the index j of the solved-for coordinate. The remaining coordinates are indexed by {i // i ≠ j}. Only the open-disc part of Definition 1.4.5 (analytic discs) is formalized, because closed analytic discs are not used here.

A complete development needs Montel's theorem for maps into bounded subsets of $\mathbb{C}^m$, homogeneous expansions and Cauchy estimates on polydiscs, the holomorphic implicit function theorem, Rouché's theorem, and holomorphic parameter-dependent Cauchy integrals. All of it is reusable beyond this mission, and contributions of it are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, §1.4–1.6 (pp. 32–46). https://www.jirka.org/scv/scv.pdf
• H. Poincaré, Les fonctions analytiques de deux variables et la représentation conforme, Rend. Circ. Mat. Palermo 23 (1907), 185–220. https://doi.org/10.1007/BF03013518
• S. G. Krantz, Function Theory of Several Complex Variables, 2nd ed., AMS Chelsea, 2001 (cited by Lebl as [K]). https://doi.org/10.1090/chel/340

Motivation

Linear second-order parabolic equations such as $u_t + Lu = f$ model diffusion with advection, growth or decay, and external sources. The heat equation is the prototype. For coefficients that are only bounded and measurable, classical solutions need not exist, and the natural well-posedness theory is the $L^2$ energy theory of weak solutions. In that theory the solution is a curve $t \mapsto u(t)$ in a Sobolev space, and the equation holds in the dual space. This framework, developed by J.-L. Lions and others in the 1950s–60s (Lions–Magenes 1972), underlies the numerical analysis of parabolic problems through finite elements and spectral Galerkin methods. It also underlies the existence theory for nonlinear evolution equations such as the Navier–Stokes equations (Temam 1977).

This mission formalizes Chapter 6 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): the existence, uniqueness and energy estimate for weak solutions of the parabolic initial–boundary value problem, proved by the Galerkin method. It also formalizes the vector-valued calculus on Hilbert triples that the proof rests on, and the Ehrling and Aubin–Lions compactness results of §6.6.

Setting

Let $\Omega \subset \mathbb{R}^n$ be a bounded open set and $T > 0$. $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$. $H^{-1}(\Omega)$ is its dual, with pairing $\langle f, v\rangle$. Every $u \in L^2(\Omega)$ acts on $H^1_0(\Omega)$ by $v \mapsto \int_\Omega uv\,dx$.

The operator is $Lu = -\sum_{i,j}\partial_i(a^{ij}\partial_j u) + \sum_j b^j\partial_j u + cu$. Its coefficients satisfy Assumption 6.1: $a^{ij}, b^j, c \in L^\infty(\Omega\times(0,T))$, $a^{ij} = a^{ji}$, and uniform ellipticity $\sum a^{ij}\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$. The associated form is

$$a(u, v; t) = \sum_{i,j}\int_\Omega a^{ij}\partial_i u\,\partial_j v\,dx + \sum_j\int_\Omega b^j\partial_j u\,v\,dx + \int_\Omega c\,uv\,dx.$$

A function $u : [0,T] \to H^1_0(\Omega)$ has weak time derivative $u_t = w$ if $\int_0^T \phi'(t)u(t)\,dt = -\int_0^T\phi(t)w(t)\,dt$ for all $\phi \in C_c^\infty(0,T)$, with Bochner integrals in $H^{-1}(\Omega)$. Given $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$, $u$ is a weak solution of

$$u_t + Lu = f \ \text{in } \Omega\times(0,T), \qquad u = 0 \ \text{on } \partial\Omega, \qquad u(0) = g$$

when three conditions hold. First, $u \in L^2(0,T;H^1_0)$ and $u_t \in L^2(0,T;H^{-1})$. Second, $\langle u_t(t), v\rangle + a(u(t), v; t) = \langle f(t), v\rangle$ for every $v \in H^1_0(\Omega)$ and a.e. $t$. Third, $u(0) = g$, where the value at $0$ is that of the continuous representative in $C([0,T];L^2(\Omega))$.

The Galerkin approximations use an $L^2$-orthonormal basis $\{w_k\}$ of Dirichlet eigenfunctions and the spaces $E_N = \langle w_1, \dots, w_N\rangle$. The approximation $u_N : [0,T] \to E_N$ solves the projected equation $(u_{Nt}, v)_{L^2} + a(u_N, v; t) = \langle f, v\rangle$ for $v \in E_N$, with $u_N(0) = P_N g$.

A Hilbert triple $\mathcal{V} \hookrightarrow \mathcal{H} \hookrightarrow \mathcal{V}'$ consists of two separable Hilbert spaces $\mathcal{V}$, $\mathcal{H}$ and the dual $\mathcal{V}'$, with dense continuous injective embeddings and $\langle f, v\rangle = (f, v)_{\mathcal{H}}$ for $f \in \mathcal{H}$. The model is $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.

Formalization targets

Goal: Theorem 6.3

For every $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$ there is a unique weak solution $u \in C([0,T];L^2) \cap L^2(0,T;H^1_0)$ with $u_t \in L^2(0,T;H^{-1})$. There is also a constant $C = C(\Omega, T, L)$ such that

$$\|u\|_{L^\infty(0,T;L^2)} + \|u\|_{L^2(0,T;H^1_0)} + \|u_t\|_{L^2(0,T;H^{-1})} \le C\big(\|f\|_{L^2(0,T;H^{-1})} + \|g\|_{L^2}\big).$$

Milestones

• Theorem 6.41. If $u \in L^2(0,T;\mathcal{V})$ and $u_t \in L^2(0,T;\mathcal{V}')$, then $u \in C([0,T];\mathcal{H})$. Moreover $\frac{d}{dt}(u,v)_{\mathcal{H}} = \langle u_t, v\rangle$, $\frac{d}{dt}\|u\|^2_{\mathcal{H}} = 2\langle u_t, u\rangle$, and $\|u\|_{L^\infty(\mathcal{H})} \le C(\|u\|_{L^2(\mathcal{V})} + \|u_t\|_{L^2(\mathcal{V}')})$.
• Theorem 6.42. $\int_0^T\langle u_t, v\rangle\,dt = (u(T),v(T))_{\mathcal{H}} - (u(0),v(0))_{\mathcal{H}} - \int_0^T\langle u, v_t\rangle\,dt$.
• Proposition 6.5. Each Galerkin problem has a unique solution $u_N$.
• Proposition 6.6. The energy estimate above holds for $u_N$ with $C$ independent of $N$.
• Proposition 6.7. A subsequence of $u_N$ converges weakly to a weak solution satisfying the estimate.
• Lemma 6.10 (Ehrling) and Theorem 6.9 (Aubin–Lions). These are further results of the chapter, stated for Banach spaces $X \hookrightarrow Y \hookrightarrow Z$ with $X$ compactly embedded in $Y$.

Significance

Theorem 6.3 is the basic well-posedness theorem for linear parabolic equations with rough coefficients. It gives existence and uniqueness, and continuous dependence on the data through the linear estimate. The same argument gives the Galerkin convergence that justifies spectral and finite-element semi-discretizations. The Hilbert-triple calculus of Theorems 6.41–6.42 is the standard setting for linear and nonlinear evolution equations. The Aubin–Lions lemma is the compactness tool for nonlinear problems, such as the semilinear heat equation of §6.6 and the Navier–Stokes equations of §6.7.

All of these results are classical and proved in the notes, except that Theorem 6.41's proof leans on vector-valued mollification. As far as a search of the platform shows, none of them is formalized there. Mathlib has the Bochner integral, $L^p$ spaces of Banach-valued functions and Gronwall's inequality. It does not have weak derivatives of vector-valued functions, Hilbert triples, or evolution-equation existence theorems. The work here is therefore to formalize known proofs, and in doing so to build reusable infrastructure for time-dependent PDEs.

Difficulty

The main obstacle is that the natural objects are equivalence classes of vector-valued functions, not functions. The initial condition $u(0) = g$ is meaningless for an element of $L^2(0,T;H^1_0)$ until Theorem 6.41 provides a continuous representative. Its proof needs extension across the endpoints and mollification of $\mathcal{V}$-valued functions. Passing to the limit in the Galerkin scheme needs weak compactness in $L^2(0,T;H^1_0)$ and $L^2(0,T;H^{-1})$, identified with a dual Bochner space. Proposition 6.5 is a linear ODE system whose coefficients are only $L^\infty$ in time, so the Picard–Lindelöf theorem for continuous right-hand sides does not apply directly. The $H^{-1}$ bound on $u_{Nt}$ needs the projection $P_N$ to be bounded on $H^1_0$ as well as on $L^2$, which is why the basis is taken to be eigenfunctions. Uniqueness needs the energy identity (6.46) and a Gronwall argument in weak form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. H10 n Ω is the closure of the jets $(\phi, \nabla\phi)$, $\phi \in C_c^\infty(\Omega)$, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, so its norm is the full $H^1$ norm. Hm1 n Ω is StrongDual ℝ (H10 n Ω). l2Embed is the embedding $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.
• $L^p(0,T;X)$ is MemLp for Lebesgue measure on $(0,T)$, and norms are eLpNorm with values in $[0,\infty]$. Constants are finite nonnegative reals. Every constant is quantified before the data it must not depend on: before $f$, $g$ in Theorem 6.3, and before the basis, $f$, $g$, $N$ in Propositions 6.6–6.7.
• The weak time derivative is (6.14) in its standard form $\int\phi' u = -\int\phi w$. The page prints $\phi$ and $\phi'$ interchanged, which is a typo.
• Weak solutions take $g \in L^2(\Omega)$ as in Assumption 6.1(3). The printed Theorem 6.3 says $g \in H^1_0(\Omega)$, a special case. $u(0) = g$ is read through a continuous representative $\tilde u \in C([0,T];L^2)$, and uniqueness means equality for a.e. $t$.
• Coefficient conditions and ellipticity hold almost everywhere on $\Omega\times(0,T)$. The Galerkin basis is a hypothesis: an orthonormal basis of $L^2(\Omega)$ of weak Dirichlet eigenfunctions.
• Proposition 6.7 states weak convergence of $u_{N_k}$ in $L^2(0,T;H^1_0)$ and of $u_{N_k t}$ in $L^2(0,T;H^{-1})$, in the explicit integral form of p. 186. This is at least as strong as the printed claim.
• Hilbert triples are structures with two continuous injective dense-range embeddings, separability, and the compatibility identity. Reflexivity in Theorem 6.9 is surjectivity of the canonical map into the bidual.
• Ruling out trivializations. Every Bochner integral in a definition has an integrable integrand under the stated $L^2$ hypotheses, so no weak-derivative or weak-solution condition holds through the integral's junk value $0$. The initial condition is imposed on a continuous representative, so it is not vacuous on a null set.
• Reusable infrastructure welcome: vector-valued mollification and extension, the Hilbert-triple calculus, and dual identification of $L^2(0,T;X)'$.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 6. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §7.1. https://doi.org/10.1090/gsm/019
• J.-L. Lions and E. Magenes, Non-Homogeneous Boundary Value Problems and Applications I, Springer, 1972. https://doi.org/10.1007/978-3-642-65161-8
• R. Temam, Navier–Stokes Equations: Theory and Numerical Analysis, North-Holland, 1977; AMS Chelsea reprint 2001. https://doi.org/10.1090/chel/343
• J. Simon, Compact sets in the space $L^p(0,T;B)$, Ann. Mat. Pura Appl. 146 (1987), 65–96. https://doi.org/10.1007/BF01762360

Motivation

Many linear partial differential equations of evolution type — the heat equation, the Schrödinger equation, linear wave and Klein–Gordon equations, linearized reaction–diffusion and Kuramoto–Sivashinsky equations — can be written as an ordinary differential equation

$$u_t = Au, \qquad u(0) = f,$$

in a Banach space $X$ of functions, where $A$ is a spatial differential operator. When $A$ is bounded, the solution is the operator exponential $e^{tA}f$. Differential operators are unbounded, however, and then the solution operators $f \mapsto u(t)$ are only continuous in time in the strong sense and may exist only forward in time. Semigroup theory makes this picture rigorous: it characterizes exactly which operators $A$ generate a well-posed evolution, and it is the standard route from energy estimates to existence and uniqueness for linear and semilinear evolution equations (Duhamel's formula, §5.4.5 of the notes, used for the semilinear heat equation in §5.5).

This mission formalizes §5.4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): uniformly continuous groups, strongly continuous semigroups and their generators, the Hille–Yosida theorem, the Lumer–Phillips theorem and Stone's theorem.

Timeline. The generation theorem for contraction semigroups is due independently to E. Hille (1948) and K. Yosida (1948); the general version with constants $M$, $a$ to Feller, Miyadera and Phillips (1952–53). G. Lumer and R. S. Phillips (1961) recast the contraction case in terms of dissipative operators. Stone's theorem on one-parameter unitary groups dates from 1930–32. Standard modern accounts are Pazy (1983) and Engel–Nagel (2000).

Setting

Let $X$ be a Banach space over $\mathbb{K} = \mathbb{R}$ or $\mathbb{C}$, and $\mathcal{L}(X)$ the Banach space of bounded linear operators on $X$ with the operator norm.

A uniformly continuous group is a family $\{T(t) : t \in \mathbb{R}\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$, and $T(h) \to I$ in operator norm as $h \to 0$. A strongly continuous (C₀) semigroup is a family $\{T(t) : t \ge 0\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$ for $s, t \ge 0$, and $T(h)f \to f$ as $h \to 0^+$ for every $f \in X$; it is a contraction semigroup if $\|T(t)\| \le 1$ for all $t \ge 0$. A C₀ group has the same properties for all $s, t \in \mathbb{R}$; on a complex Hilbert space it is unitary if every $T(t)$ is unitary.

An operator $A : \mathcal{D}(A) \subset X \to X$ is a linear map defined on a subspace $\mathcal{D}(A)$. The generator of a C₀ semigroup is the operator $A$ whose domain is the set of $f$ for which

$$Af = \lim_{h \to 0^+} \frac{T(h)f - f}{h}$$

exists in norm, with $Af$ this limit. $A$ is closed if its graph $\{(f, Af) : f \in \mathcal{D}(A)\}$ is closed in $X \times X$, and densely defined if $\mathcal{D}(A)$ is dense. A scalar $\lambda$ is in the resolvent set of $A$ if $\lambda I - A : \mathcal{D}(A) \to X$ is a bijection, and then $R(\lambda, A) = (\lambda I - A)^{-1}$ is the resolvent. $A$ is dissipative if $\lambda\|f\| \le \|(\lambda I - A)f\|$ for all real $\lambda > 0$ and $f \in \mathcal{D}(A)$, and m-dissipative if in addition $\lambda I - A$ is onto $X$ for some $\lambda > 0$. On a complex Hilbert space $\mathcal{H}$, $A$ is self-adjoint if $\mathcal{D}(A)$ is dense, $\mathcal{D}(A) = \mathcal{D}(A^*)$, and $(x, Ay) = (Ax, y)$ for $x, y \in \mathcal{D}(A)$.

Formalization targets

Goal: the Lumer–Phillips theorem (Theorem 5.38)

For an operator $A : \mathcal{D}(A) \subset X \to X$,

$$A \text{ generates a C₀ contraction semigroup on } X \iff A \text{ is closed, densely defined and m-dissipative.}$$

Milestones

1. Theorem 5.24. A uniformly continuous group is smooth in operator norm, $A = T'(0) \in \mathcal{L}(X)$ exists, and $T(t) = e^{tA}$ for all $t \in \mathbb{R}$.
2. Theorem 5.32. The generator of a C₀ semigroup is closed and densely defined.
3. Theorem 5.35 (Hille–Yosida). $A$ generates a C₀ semigroup if and only if, for some $M \ge 1$ and $a \in \mathbb{R}$, $A$ is closed and densely defined, $(a, \infty)$ lies in the resolvent set, and

$$\|R(\lambda, A)^n\| \le \frac{M}{(\lambda - a)^n} \qquad (\lambda > a,\ n \in \mathbb{N});$$

in that case $\|T(t)\| \le M e^{at}$ for $t \ge 0$. 4. Corollary 5.36. The contraction case: $M = 1$, $a = 0$, with $\|R(\lambda, A)\| \le 1/\lambda$. 5. Theorem 5.42 (Stone). On a complex Hilbert space, $iA$ generates a C₀ unitary group if and only if $A$ is self-adjoint.

Significance

The result itself. The Lumer–Phillips theorem is the working form of generation theory for PDEs: to show that $u_t = Au$ is well posed with $\|u(t)\| \le \|u(0)\|$, it suffices to prove an energy inequality (dissipativity) and to solve a single resolvent equation $\lambda f - Af = g$. The notes apply it to the Laplacian on $H^2(\mathbb{R}^n) \subset L^2(\mathbb{R}^n)$ and, after a shift, to the linearized Kuramoto–Sivashinsky operator; later chapters use the resulting semigroups in Duhamel's formula to construct solutions of semilinear heat and Schrödinger equations. Hille–Yosida gives the general growth bound $\|T(t)\| \le Me^{at}$, and Stone's theorem identifies unitary quantum dynamics with self-adjoint Hamiltonians.

Formalizing it. All results are classical and proved in the literature; the notes themselves state 5.32, 5.35, 5.36, 5.38 and 5.42 without proof, referring to standard texts. Mathlib currently has the operator exponential on Banach algebras, partially defined linear maps (LinearPMap) with closedness, closures and adjoints, but no theory of C₀ semigroups or their generators. A complete development would give Lean a reusable generation theory for unbounded operators, on which parabolic and dispersive PDE existence results can rest.

Difficulty

The central obstacle is the passage from resolvent information to a semigroup. Formally $T(t) = e^{tA}$, but for unbounded $A$ the exponential series is meaningless, and the necessity directions require showing that the resolvent is a Laplace transform of the semigroup, which needs integration of strongly (not norm) continuous operator-valued functions. The sufficiency directions must construct a semigroup from $A$ by an approximation of the unbounded generator and a limit that converges only strongly, and then identify the generator of the limit with $A$ — including its domain, which is where most careless arguments fail. In the Lumer–Phillips theorem, surjectivity of $\lambda I - A$ is assumed for a single $\lambda > 0$ and must be propagated to every $\lambda > 0$. In Stone's theorem both directions need domain arguments for unbounded operators on Hilbert space; symmetry of $A$ alone is not enough.

Formalization scope

• Scalars: a field 𝕜 with [RCLike 𝕜] (ℝ or ℂ), and X a Banach space over it ([NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X]). Stone's theorem is over ℂ on an InnerProductSpace ℂ H with [CompleteSpace H]. Theorem 5.24 additionally equips X with a compatible real structure ([NormedSpace ℝ X] [IsScalarTower ℝ 𝕜 X]) so that $t \mapsto T(t)$ can be differentiated; $e^{tA}$ is Mathlib's NormedSpace.exp, and $C^\infty$ is ContDiff ℝ ∞.
• Operators $A : \mathcal{D}(A) \subset X \to X$ are X →ₗ.[𝕜] X (LinearPMap); closedness is LinearPMap.IsClosed (closed graph).
• Semigroups are functions T : ℝ → X →L[𝕜] X; for semigroups only the values at $t \ge 0$ enter. Composition is multiplication in X →L[𝕜] X.
• The generator relation IsGenerator T A states, for all $f, g$: the right difference quotient $h^{-1}(T(h)f - f)$ tends to $g$ as $h \to 0^+$ if and only if $f \in \mathcal{D}(A)$ and $Af = g$. So "$A$ generates a semigroup" means that $A$ equals the generator including its domain; a formalization in which $A$ merely agrees with the limit on some subspace, or in which the generator is a restriction, would make the theorems different (and false) statements, and is ruled out.
• Resolvent norm bounds $\|R(\lambda, A)^n\| \le c$ are stated pointwise, $\|R(\lambda,A)^n g\| \le c\|g\|$ for all $g$, which is equivalent. In (5.24) $n = 0$ is included, which adds nothing because $M \ge 1$. The "in that case" clause of Theorem 5.35 is a second conjunct: for every semigroup generated by $A$ and every $M, a$ satisfying the three conditions, $\|T(t)\| \le Me^{at}$.
• Closedness and density, which the notes build into the definitions of the resolvent set and of dissipativity, are stated explicitly wherever they are used (they appear as condition (1) in every theorem).
• The generator of a C₀ group (Stone) is the generator of its forward part, as in Definition 5.30; the operator $iA$ is Complex.I • A, with the same domain as $A$. Self-adjointness is Definition 5.41 as printed, not Mathlib's IsSelfAdjoint for LinearPMap, although the two agree.
• Useful infrastructure, reusable beyond this mission: Riemann/Bochner integration of strongly continuous operator families, the Laplace-transform representation of the resolvent, Yosida approximations, and dissipativity–resolvent equivalences. 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, §5.4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Springer GTM 194, 2000. https://doi.org/10.1007/b97696
• G. Lumer and R. S. Phillips, Dissipative operators in a Banach space, Pacific J. Math. 11 (1961), 679–698. https://doi.org/10.2140/pjm.1961.11.679
• M. H. Stone, On one-parameter unitary groups in Hilbert space, Ann. of Math. 33 (1932), 643–648. https://doi.org/10.2307/1968538
• K. Yosida, On the differentiability and the representation of one-parameter semigroup of linear operators, J. Math. Soc. Japan 1 (1948), 15–21. https://doi.org/10.2969/jmsj/00110015