Analysis

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 7.8

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Why relatively bounded perturbations matter

A quantum-mechanical Hamiltonian is usually a sum $H = H_0 + V$ of a kinetic energy $H_0$ (for a free particle, $H_0 = -\Delta$ in units with $\hbar = 1$, $m = 1/2$) and a potential energy $V$. Observables must be self-adjoint operators, not merely symmetric ones: only then does the spectral theorem apply and the time evolution $e^{-itH}$ exist as a unitary group. Self-adjointness of $H_0$ is usually a direct computation. For the sum it is not, because $H_0$ and $V$ are unbounded, and the sum of two self-adjoint unbounded operators need not be self-adjoint or even densely defined.

The Kato–Rellich theorem settles this when $V$ is small compared with $H_0$ in a precise sense. The result goes back to Rellich's perturbation theory of spectral decompositions (see the notes to Section V.4 of Kato's monograph), and Kato used it in 1951 (Trans. AMS 70, 195–211) to prove that atomic Hamiltonians with Coulomb interactions are self-adjoint. It is the standard first tool in the mathematical theory of Schrödinger operators. This mission formalizes Section 6.1 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the notion of relative boundedness, its characterizations, the theorem itself, and the second resolvent formula.

Setting

Let $\mathfrak{H}$ be a complex Hilbert space with inner product $\langle\cdot,\cdot\rangle$, conjugate-linear in the first slot. A linear operator $A$ is a linear map $A : \mathfrak{D}(A) \to \mathfrak{H}$ defined on a subspace $\mathfrak{D}(A) \subseteq \mathfrak{H}$, its domain. The sum $A + B$ is defined on $\mathfrak{D}(A) \cap \mathfrak{D}(B)$. $A$ is symmetric if $\mathfrak{D}(A)$ is dense and $\langle \varphi, A\psi\rangle = \langle A\varphi, \psi\rangle$ for $\varphi, \psi \in \mathfrak{D}(A)$. It is self-adjoint if it equals its adjoint $A^*$, domains included, and essentially self-adjoint if its closure $\overline{A}$ (the operator whose graph is the closure of the graph of $A$) is self-adjoint. $A$ is bounded from below by $\gamma \in \mathbb{R}$ if $\langle\psi, A\psi\rangle \ge \gamma\|\psi\|^2$ for all $\psi \in \mathfrak{D}(A)$.

The resolvent set $\rho(A)$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak{D}(A) \to \mathfrak{H}$ is a bijection with bounded inverse $R_A(z) = (A - z)^{-1}$, the resolvent.

An operator $B$ is $A$ bounded if $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and there are constants $a, b \ge 0$ with

$$\|B\psi\| \le a\|A\psi\| + b\|\psi\|, \qquad \psi \in \mathfrak{D}(A). \tag{6.1}$$

The $A$-bound of $B$ is the infimum of the admissible $a$. If $B$ is $A$ bounded, the product $BR_A(z)$ is defined on all of $\mathfrak{H}$ for $z \in \rho(A)$.

Formalization targets

Goal: the Kato–Rellich theorem (Theorem 6.4, self-adjoint case)

Let $A$ be self-adjoint and $B$ symmetric with $A$-bound less than one. Then

$$A + B \text{ with } \mathfrak{D}(A + B) = \mathfrak{D}(A) \text{ is self-adjoint,}$$

and if $A$ is bounded from below by $\gamma$ and (6.1) holds with constants $a \in [0,1)$ and $b \ge 0$, then

$$A + B \ \ge\ \gamma - \max\Big(a|\gamma| + b,\ \frac{b}{1-a}\Big).$$

The printed form of (6.3) has $b/(a-1)$ where this statement has $b/(1-a)$. The printed version is false: a two-dimensional example with $\gamma = 0$, $a \approx 0.93$, $b \approx 5.97$ has lowest eigenvalue of $A + B$ about $-6.66 < -b$. The corrected constant is the one in Kato's monograph (Theorem V.4.11). The lower bound is stated for every admissible pair $(a, b)$, not for the $A$-bound itself, which is an infimum and need not be attained.

Milestones

1. Lemma 6.1. $A$ bounded operators form a linear space, and the $A$-bound of $\alpha_1 B_1 + \alpha_2 B_2$ is at most $|\alpha_1| a_1 + |\alpha_2| a_2$.
2. Lemma 6.2. For $A$ closed with nonempty resolvent set and $B$ closable, the following are equivalent: $B$ is $A$ bounded; $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$; $BR_A(z)$ is bounded for one $z \in \rho(A)$; $BR_A(z)$ is bounded for all $z \in \rho(A)$. The $A$-bound is at most $\inf_{z \in \rho(A)} \|BR_A(z)\|$.
3. Lemma 6.3. For $A$ self-adjoint and $B$ $A$ bounded, the $A$-bound equals $\lim_{\lambda\to\infty}\|BR_A(\pm i\lambda)\|$, and also $\lim_{\lambda\to\infty}\|BR_A(-\lambda)\|$ when $A$ is bounded from below.
4. Theorem 6.4, essentially self-adjoint case. For $A$ essentially self-adjoint and $B$ symmetric with $A$-bound less than one, $A + B$ is essentially self-adjoint, $\mathfrak{D}(\overline{A}) \subseteq \mathfrak{D}(\overline{B})$ and $\overline{A + B} = \overline{A} + \overline{B}$, with the same lower bound.
5. Lemma 6.5. For closed $A$, $B$ with $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $z \in \rho(A) \cap \rho(A+B)$,

$$R_{A+B}(z) - R_A(z) = -R_A(z) B R_{A+B}(z) = -R_{A+B}(z) B R_A(z).$$

Significance

Kato–Rellich is the entry point to self-adjointness of Schrödinger operators. With the Sobolev estimates of later chapters it gives self-adjointness of $-\Delta + V$ on $H^2(\mathbb{R}^3)$ for $V \in L^2 + L^\infty$, which covers the hydrogen atom and, through the $N$-body extension, every atom and molecule with Coulomb interactions. The lower bound (6.3) says the perturbed Hamiltonian is still bounded from below, which is the mathematical form of stability of the ground state. The second resolvent formula is used throughout perturbation theory: to compare spectra (Weyl's theorem on essential spectra), to study resolvent convergence, and in scattering theory.

In a formal library, relative boundedness is the shared layer on which every later statement about Schrödinger operators rests. Mathlib has unbounded operators (LinearPMap), their adjoints and closures, but no relative boundedness, no resolvent of an unbounded operator, and no perturbation theorem for self-adjointness. The theorem is textbook material and has been proved many times; what does not yet exist is a machine-checked proof for unbounded operators in this generality.

Difficulty

Self-adjointness of $A + B$ is a statement about the adjoint $(A+B)^*$, whose domain is defined implicitly. The inclusion $A + B \subseteq (A + B)^*$ follows from symmetry, but the reverse inclusion does not come from any manipulation on $\mathfrak{D}(A)$. It requires knowing that certain ranges are all of $\mathfrak{H}$, and that range information is not visible from the inequality (6.1) alone. Relating the $A$-bound, an infimum over constants in an inequality on $\mathfrak{D}(A)$, to norms of the bounded operators $BR_A(z)$ is where the self-adjointness of $A$ enters. For the essentially self-adjoint case, the domains of three different closures have to be compared. For the lower bound, the constant depends on $a$ and $b$ in two regimes, and the printed version of the formula gets one regime wrong.

Formalization scope

• Hilbert space. {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed and not needed.
• Operators are LinearPMaps H →ₗ.[ℂ] H; $A + B$ is Mathlib's sum on the intersection of the domains; closures are LinearPMap.closure; self-adjointness is Mathlib's IsSelfAdjoint; symmetric operators include density of the domain.
• Relative bounds. IsRelativelyBoundedWith A B a b contains the domain inclusion $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $a, b \ge 0$. The $A$-bound relativeBound A B is valued in $[0,\infty]$ and equals $\infty$ exactly when $B$ is not $A$ bounded, so "$A$-bound less than one" cannot hold vacuously.
• Resolvents. $\rho(A)$ and $R_A(z)$ are defined for arbitrary operators as in Teschl (2.66): a bounded, everywhere defined two-sided inverse of $A - z$. Mathlib's Banach-algebra spectrum is not used. resolvent A z is $0$ off $\rho(A)$, and statements use it only at points of $\rho(A)$ or eventually along rays that lie in $\rho(A)$.
• Norms of possibly unbounded operators (opNorm) are valued in $[0,\infty]$; "$BR_A(z)$ is bounded" means everywhere defined with finite norm.
• Additions to the printed statements. Lemma 6.2 carries $\rho(A) \neq \emptyset$, without which its "for one $z$" clause is unsatisfiable. Lemma 6.1's "less than" is stated as "at most". (6.3) uses $b/(1-a)$.
• Ruling out trivialization. The hypotheses of the goal are only: $A$ self-adjoint, $B$ symmetric, and $A$-bound less than one. No hypothesis that $A + B$ is closed, that $\operatorname{Ran}(A + B \pm i) = \mathfrak{H}$, or that $\pm i \in \rho(A+B)$ appears, since any of these would assume the conclusion.

A complete development needs basic facts about resolvents of self-adjoint operators ($\pm i\lambda \in \rho(A)$ and the norm estimates for $R_A$), the closed graph theorem for closable operators, and Neumann series. All of these are reusable in later missions of this series: Weyl's theorem, the free Schrödinger operator, atomic Hamiltonians. Contributions that build these as general LinearPMap lemmas are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Section 6.1. https://doi.org/10.1090/gsm/099
• T. Kato, Perturbation Theory for Linear Operators, Springer, 2nd ed. 1976, Section V.4. https://doi.org/10.1007/978-3-642-66282-9
• T. Kato, "Fundamental properties of Hamiltonian operators of Schrödinger type", Trans. Amer. Math. Soc. 70 (1951), 195–211. https://doi.org/10.1090/S0002-9947-1951-0041010-X
• M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, Theorem X.12. ISBN 978-0-12-585002-5

Motivation

A second-order elliptic equation in divergence form, $Lu = -\sum_{i,j}\partial_i(a_{ij}\partial_j u) = f$, is usually solved in a weak sense: the Lax–Milgram theorem or the Fredholm alternative produces a function $u \in H^1(\Omega)$, which has only first-order weak derivatives, and the equation holds after one integration by parts against every test function. The phrase "solution of a PDE" then covers objects for which the second derivatives appearing in $L$ need not exist. Regularity theory closes this gap: under smoothness of the coefficients and the data, weak solutions have exactly as many derivatives as the equation suggests. It is used throughout the calculus of variations, spectral theory and nonlinear PDE.

The interior $H^2$ estimate for divergence-form operators with $C^1$ coefficients goes back to the difference-quotient technique of L. Nirenberg (1955) and is standard in textbooks such as Evans, Partial Differential Equations, §6.3, and Gilbarg–Trudinger, Chapter 8. This mission follows the treatment in J. K. Hunter's lecture notes, §4.11 and Appendix 4.C.

Setting

Points of $\mathbb{R}^n$ are written $x = (x_1, \dots, x_n)$, and $e_i$ is the $i$th standard unit vector. Let $\Omega \subseteq \mathbb{R}^n$ be an open set. A set $\Omega'$ is compactly contained in $\Omega$, written $\Omega' \Subset \Omega$, if $\Omega'$ is nonempty and open, its closure $\overline{\Omega'}$ is compact, and $\overline{\Omega'} \subset \Omega$.

A test function is an infinitely differentiable $\phi$ with compact support inside $\Omega$ (the space $C_c^\infty(\Omega)$). A function $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ (multi-index $\alpha$) if $\int_\Omega g\phi\,dx = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi\,dx$ for all test functions $\phi$. The Sobolev space $H^k(\Omega) = W^{k,2}(\Omega)$ consists of the functions whose weak derivatives of order at most $k$ exist and lie in $L^2(\Omega)$, with norm $\|u\|_{H^k(\Omega)} = (\sum_{|\alpha|\le k}\|\partial^\alpha u\|_{L^2(\Omega)}^2)^{1/2}$; more generally $W^{k,p}(\Omega)$ uses $L^p$. The space $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in $H^1(\Omega)$.

The coefficients are functions $a_{ij}$, $1 \le i, j \le n$, which are bounded ($a_{ij} \in L^\infty(\Omega)$), symmetric ($a_{ij} = a_{ji}$) and uniformly elliptic: for some $\theta > 0$,

$$\sum_{i,j=1}^n a_{ij}(x)\xi_i\xi_j \ge \theta|\xi|^2 \quad\text{for a.e. } x \in \Omega \text{ and all } \xi \in \mathbb{R}^n.$$

Given $f \in L^2(\Omega)$, a function $u \in H^1(\Omega)$ is a weak solution of $Lu = f$ if

$$a(u, v) := \sum_{i,j=1}^n \int_\Omega a_{ij}\,\partial_i u\,\partial_j v\,dx = \int_\Omega f v\,dx \quad \text{for all } v \in H^1_0(\Omega).$$

No boundary condition is imposed on $u$.

For $h \ne 0$ the $i$th difference quotient of $u : \mathbb{R}^n \to \mathbb{R}$ is $D_i^h u(x) = (u(x + he_i) - u(x))/h$, and $D^h u = (D_1^h u, \dots, D_n^h u)$ with pointwise length $|D^h u| = (\sum_i (D_i^h u)^2)^{1/2}$.

Formalization targets

Goal: interior $H^2$ regularity (Theorem 4.27)

If moreover $a_{ij} \in C^1(\Omega)$, then for every $\Omega' \Subset \Omega$ there is a constant $C$, depending only on $n$, $\Omega'$, $\Omega$ and the coefficients, such that every weak solution $u$ of $Lu = f$ with $f \in L^2(\Omega)$ satisfies $u \in H^2(\Omega')$ and

$$\|u\|_{H^2(\Omega')} \le C\big(\|f\|_{L^2(\Omega)} + \|u\|_{L^2(\Omega)}\big).$$

Milestones: difference quotients (Appendix 4.C)

• Proposition 4.52 (1): if $u$ and its weak derivative $\partial_i u$ are locally integrable on $\mathbb{R}^n$, then $\partial_i D_j^h u = D_j^h\partial_i u$.
• Proposition 4.52 (2): for $u \in L^p(\mathbb{R}^n)$, $v \in L^{p'}(\mathbb{R}^n)$, $1 \le p \le \infty$, $\int (D_i^h u)\,v\,dx = -\int u\,(D_i^{-h}v)\,dx$.
• Theorem 4.53 (1): with $d = \operatorname{dist}(\Omega', \partial\Omega)$, $1 \le p < \infty$ and $0 < |h| < d$, $\|D_i^h u\|_{L^p(\Omega')} \le \|\partial_i u\|_{L^p(\Omega)}$ for each $i$.
• Theorem 4.53 (2): if $u \in L^p(\Omega)$, $1 < p < \infty$, and $\|D^h u\|_{L^p(\Omega')} \le C$ for all $0 < |h| < d/2$, then $u \in W^{1,p}(\Omega')$ and $\|Du\|_{L^p(\Omega')} \le C$.

Stronger targets

• Theorem 4.28: if $a_{ij} \in C^{k+1}(\Omega)$ and $f \in H^k(\Omega)$, then $u \in H^{k+2}(\Omega')$ with $\|u\|_{H^{k+2}(\Omega')} \le C(\|f\|_{H^k(\Omega)} + \|u\|_{L^2(\Omega)})$, $C$ depending only on $n, k, \Omega', \Omega$ and the coefficients.
• Corollary 4.29: if $a_{ij}, f \in C^\infty(\Omega)$, then $u$ agrees a.e. in $\Omega$ with a $C^\infty(\Omega)$ function.

Significance

The goal theorem shows that weak solutions of divergence-form equations with $C^1$ coefficients are strong solutions: their second weak derivatives are square integrable on compact subsets, so the equation $Lu = f$ holds pointwise almost everywhere. The iterated version (Theorem 4.28) and its corollary turn the existence theory for weak solutions into existence of smooth solutions whenever the coefficients and data are smooth; in combination with Sobolev embedding this is how one proves that eigenfunctions of the Dirichlet Laplacian on an open set are smooth in its interior.

All of these results are classical and fully proved in the literature. To the best of the platform's records, none is formalized: Mathlib has Lebesgue spaces, Fréchet derivatives and Hilbert-space tools, but neither weak derivatives nor Sobolev spaces on open sets, and there is no elliptic regularity result in any proof assistant known to the maintainers. A complete development would therefore also deliver reusable infrastructure: weak derivatives, $W^{k,p}(\Omega)$ and its norm, difference quotients and their calculus, and cut-off functions subordinate to $\Omega' \Subset \Omega$.

Difficulty

The formal computation behind the estimate — testing the equation against $-\partial_k(\eta^2\partial_k u)$ for a cut-off $\eta$ and using ellipticity — is illegitimate for a weak solution, because the test function involves second derivatives of $u$ that are not yet known to exist. Replacing derivatives by difference quotients makes every step meaningful but requires a separate theory: commuting difference quotients with weak derivatives, a discrete product rule and integration by parts, and a compactness argument in $L^p$ (reflexivity) that turns an $h$-uniform bound into a weak derivative. The error terms involve difference quotients of the coefficients, which is where $a_{ij} \in C^1$ enters, and the final estimate has to be closed with a Cauchy inequality and a second localization to replace $\|u\|_{H^1}$ by $\|u\|_{L^2}$.

Formalization scope

Space is $\mathbb{R}^n$ = EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; coordinates are 0-based (i : Fin n), so the book's $e_1, \dots, e_n$ are EuclideanSpace.single 0 1, …. Functions are real-valued on all of $\mathbb{R}^n$ and only their values on the relevant open set matter. Weak derivatives (HasWeakDeriv, weakDeriv), $W^{k,p}(\Omega)$ (MemW), its norm (sobolevNorm, valued in ℝ≥0∞) and $W^{k,p}_0(\Omega)$ (MemW0) are defined in the mission; weakDeriv is a chosen representative and is only used under hypotheses guaranteeing existence. Exponents are p : ℝ≥0∞; conjugate exponents use ENNReal.HolderConjugate. $C^k(\Omega)$ and $C^\infty(\Omega)$ are ContDiffOn ℝ k and ContDiffOn ℝ ∞ on $\Omega$ (smooth, not analytic); "$u \in C^\infty(\Omega)$" for a Sobolev function means a.e. equality on $\Omega$ with such a function.

Conventions committed to:

• The standing assumptions of §4.6 on the operator — $a_{ij} \in L^\infty(\Omega)$, $a_{ij} = a_{ji}$, uniform ellipticity — are explicit hypotheses of Theorems 4.27–4.29, and $f \in L^2(\Omega)$ (the setting (4.34)) is a hypothesis of Corollary 4.29.
• Theorem 4.27 assumes $a_{ij} \in C^1(\Omega)$ as printed, not $C^1(\overline{\Omega})$.
• Constants: ∃ C : ℝ is quantified after $\Omega$, the coefficients, the ellipticity constant and $\Omega'$ (and $k$), and before $f$ and $u$.
• $\operatorname{dist}(\Omega', \partial\Omega)$ in Theorem 4.53 is modelled by any $d > 0$ with $B(x, d) \subseteq \Omega$ for all $x \in \Omega'$; the largest such $d$ is the book's distance (and $+\infty$ when $\Omega = \mathbb{R}^n$), so this is the book's condition and avoids Lean's convention that the distance to the empty set is $0$.
• Two corrections of the printed statements: Proposition 4.52 (2) is stated with $D_i^{-h}v$ on the right, as the book's proof derives; Theorem 4.53 (1) is stated componentwise, $\|D_i^h u\|_{L^p(\Omega')} \le \|\partial_i u\|_{L^p(\Omega)}$, which is what its proof establishes and what the proof of Theorem 4.27 uses (the printed vector form with Euclidean lengths fails for large $p$, e.g. for $u = \max(x_1, x_2)$).

The theorems are not trivialized by junk values: the difference quotient is only used at $h \ne 0$, the weak formulation's Bochner integrals are integrable under the stated $L^\infty$ and $L^2$ hypotheses, and the conclusion $u \in H^2(\Omega')$ asserts existence of all weak derivatives of order at most two, not merely a bound on a norm that could be computed from junk representatives.

Contributions welcome: a library of weak derivatives and Sobolev spaces on open subsets of $\mathbb{R}^n$ compatible with these definitions, cut-off functions for $\Omega' \Subset \Omega$ (Mathlib's ContDiffBump and exists_smooth_tsupport_subset are natural starting points), and Banach–Alaoglu for $L^p$, $1 < p < \infty$.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §4.11 and Appendix 4.C. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, American Mathematical Society, 2010, §5.8.2 and §6.3. https://doi.org/10.1090/gsm/019
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Classics in Mathematics, Springer, 2001, §7.11 and §8.3. https://doi.org/10.1007/978-3-642-61798-0
• L. Nirenberg, Remarks on strongly elliptic partial differential equations, Communications on Pure and Applied Mathematics 8 (1955), 649–675. https://doi.org/10.1002/cpa.3160080414

Why regular Sturm–Liouville problems

Separation of variables reduces the heat equation, the wave equation and the Schrödinger equation on an interval to an eigenvalue problem for a second-order ordinary differential operator with boundary conditions at both ends. Whether the method works depends on one fact: the eigenfunctions of that operator must be complete, so that every reasonable initial profile can be expanded in them. Chapter 5 of Gerald Teschl's Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) proves this for regular Sturm–Liouville problems. It does so without Lebesgue integration or Hilbert-space completeness: it works in the space of continuous functions with a weighted scalar product, and it develops the necessary spectral theory of compact symmetric operators from scratch.

A short history. Sturm and Liouville (1836–1837) studied the zeros and the eigenvalues of such equations and the expansion of functions in eigenfunctions. Hilbert and Schmidt (1904–1907) put the expansion on a rigorous footing through their theory of integral equations with symmetric kernels, from which the abstract spectral theorem for compact symmetric operators emerged.

Setting

Let $a < b$ and let $p, q, r$ be real functions on $[a,b]$ with

$$r, q \in C([a,b], \mathbb{R}), \qquad p \in C^1([a,b], \mathbb{R}), \qquad p(x) > 0,\ r(x) > 0 \ \ (x \in [a,b]). \qquad (5.45)$$

These regularity assumptions hold throughout. The Sturm–Liouville operator is

$$L f = \frac{1}{r}\Bigl( -(p f')' + q f \Bigr),$$

acting on the domain

$$D(L) = \{ f \in C^2([a,b], \mathbb{C}) : \cos(\alpha) f(a) - \sin(\alpha) p(a) f'(a) = 0,\ \ \cos(\beta) f(b) - \sin(\beta) p(b) f'(b) = 0 \}$$

for fixed real $\alpha, \beta$ (the separated boundary conditions; $\alpha = 0$ is Dirichlet, $\alpha = \pi/2$ Neumann). The underlying space is $H_0 = C([a,b], \mathbb{C})$ with the weighted scalar product

$$\langle f, g \rangle = \int_a^b f(x)^* g(x)\, r(x)\, dx$$

and norm $\|f\| = \sqrt{\langle f, f\rangle}$. $H_0$ is an inner product space but it is not complete. A number $z \in \mathbb{C}$ is an eigenvalue of $L$ if $L f = z f$ for some $f \in D(L)$ that does not vanish identically; $f$ is an eigenfunction. An orthonormal basis of $H_0$ is an orthonormal sequence $(u_n)$ such that $\|f - \sum_{n<N} \langle u_n, f\rangle u_n\| \to 0$ for every $f \in H_0$.

For the abstract part, $H_0$ is any complex inner product space (again not assumed complete). A linear operator $A$ on a dense subspace is symmetric if $\langle g, Af\rangle = \langle Ag, f\rangle$; an everywhere defined $A$ is compact if $(A f_n)$ has a convergent subsequence in $H_0$ whenever $(f_n)$ is bounded.

For $z \in \mathbb{C}$ let $u_a(z,\cdot)$, $u_b(z,\cdot)$ solve $L u = z u$ with $u_a(z,a) = \sin\alpha$, $p(a)u_a'(z,a) = \cos\alpha$, $u_b(z,b) = \sin\beta$, $p(b)u_b'(z,b) = \cos\beta$. Their Wronskian is $W(z) = u_b p u_a' - p u_b' u_a$, which does not depend on the point where it is evaluated. When $W(z) \neq 0$, the resolvent $R_L(z)$ is the integral operator with the Green function $G(z,x,t) = W(z)^{-1} u_b(z,\max(x,t))\, u_a(z,\min(x,t))$ and weight $r$.

Formalization targets

Goal: eigenfunction expansion (Theorem 5.11)

There are real numbers $E_n$ and real-valued eigenfunctions $u_n \in D(L)$, $L u_n = E_n u_n$, such that:

• the $E_n$ are pairwise distinct and are all the eigenvalues of $L$, and every eigenfunction for $E_n$ is a multiple of $u_n$ (the eigenvalues are simple);
• $|E_n| \to \infty$ (the eigenvalues accumulate only at $\infty$);
• $\langle u_m, u_n \rangle = \delta_{mn}$, and for every $f \in H_0$

$$f = \sum_{n=0}^{\infty} \langle u_n, f \rangle\, u_n \quad \text{in } H_0, \qquad (5.70)$$

• for $f \in D(L)$ the series (5.70) converges uniformly on $[a,b]$.

Milestones

1. Theorem 5.4. Eigenvalues of a symmetric operator are real, and eigenvectors for different eigenvalues are orthogonal.
2. Theorem 5.5. A compact symmetric operator on a nonzero inner product space has an eigenvalue $\alpha_0$ with $|\alpha_0| = \|A\| = \sup_{\|f\|=1}\|Af\|$.
3. Theorem 5.6 (spectral theorem). A compact symmetric operator has real eigenvalues $\alpha_j$ with orthonormal eigenvectors $u_j$, infinitely many when $H_0$ is infinite dimensional and then $\alpha_j \to 0$, and $f = \sum_j \langle u_j, f\rangle u_j$ for every $f \in \operatorname{Ran}(A)$; if $\operatorname{Ran}(A)$ is dense the $u_j$ are an orthonormal basis.
4. Lemma 5.9. $W(z)$ is an entire function of $z$ whose zeros are exactly the eigenvalues of $L$.
5. Lemma 5.10. For $W(z) \ne 0$, $R_L(z)$ is compact on $H_0$, and symmetric for real $z$.
6. Lemma 5.12 (Rayleigh–Ritz). The eigenvalues can be ordered $E_0 < E_1 < \cdots$; $E_0 = \min \langle f, Lf\rangle = \min Q(f)$ over normalized $f \in D(L)$, attained exactly at the eigenfunctions for $E_0$; and $\min_{[a,b]} q \le E_0$ when $0 \le \alpha \le \pi/2 \le \beta \le \pi$. Here $Q$ is the quadratic form $\int_a^b (p |f'|^2 + q |f|^2)\,dx$ plus the boundary terms $\cot(\alpha)|f(a)|^2 - \cot(\beta)|f(b)|^2$ (dropped when the angle is $0$).

Significance

Theorem 5.11 is the statement that makes eigenfunction expansions legitimate: Fourier sine and cosine series are its special case $p = r = 1$, $q = 0$, and it covers any positive weight and any smooth positive stiffness with separated boundary conditions. Solutions of the heat and wave equations on an interval with variable coefficients are built from it. The uniform convergence for $f \in D(L)$ is the version needed to differentiate or evaluate such series pointwise. Lemma 5.12 provides the variational characterisation of the lowest eigenvalue, the starting point for comparison theorems and eigenvalue estimates.

On the formal side, Mathlib has the spectral theorem for self-adjoint operators on finite-dimensional spaces, compact operators on normed spaces, and $L^2$ spaces. It has no Sturm–Liouville theory, no Green functions for boundary value problems, and no spectral theorem for compact symmetric operators on incomplete inner product spaces. The platform has finite-dimensional Rayleigh-quotient results and compactness of $L^2$ convolution operators, but nothing on this setting. The results here are classical and proved; what is missing is a machine-checked proof in the book's elementary setting of continuous functions.

Difficulty

The operator $L$ is unbounded on $H_0$ (Problem 5.16), so the obvious first idea, applying a spectral theorem for compact or bounded symmetric operators to $L$ itself, does not work. Completeness of the eigenfunctions is also subtle because $H_0$ is not complete. Hilbert-space arguments that produce limits in a completion, or that go through $L^2$, do not by themselves give an expansion of a continuous function in continuous eigenfunctions with convergence in $H_0$, still less uniform convergence. Simplicity of the eigenvalues depends on the separated boundary conditions and fails for periodic ones. On the formal side, one needs analytic dependence of solutions of a linear ODE on a complex parameter, one-sided derivatives at the endpoints, and interval integrals of piecewise-defined kernels.

Formalization scope

• Spaces. The abstract results use a type with [NormedAddCommGroup E] [InnerProductSpace ℂ E] and no CompleteSpace. Symmetry on a dense domain is IsSymmetricOp; for everywhere defined operators it is Mathlib's LinearMap.IsSymmetric. Compactness is IsCompactOp: subsequences converge in $H_0$ itself. $H_0 = C([a,b],\mathbb{C})$ is represented by functions $\mathbb{R} \to \mathbb{C}$ continuous on Set.Icc a b, with SLInner the weighted scalar product (5.52) as an interval integral. It is not $L^2$ and not a HilbertBasis.
• Operator and domain. SLOp, SLDomain, IsSLEigenfunction implement (5.53)–(5.55) with derivWithin on Set.Icc a b (one-sided at the endpoints) and ContDiffOn ℝ 2. RegularSL is (5.45), including $a < b$. $\alpha, \beta$ are arbitrary reals.
• Quantifier readings. "Countable, discrete, accumulating only at $\infty$" is an injective sequence $E_n$ exhausting the eigenvalues with $|E_n| \to \infty$. "Simple" is: every eigenfunction for $E_n$ equals $c\,u_n$ on $[a,b]$. "Can be chosen real-valued" is an existential choice of $u_n : \mathbb{R} \to \mathbb{R}$. $\|A\|$ in Theorem 5.5 is expressed by IsLUB of $\{\|Af\| : \|f\|=1\}$, and Theorem 5.5 assumes $H_0 \neq \{0\}$. In Theorem 5.6, $N \in \mathbb{N}_0 \cup \{\infty\}$ is ℕ∞: $N = \infty$ in infinite dimension and $N = \dim H_0$ otherwise. The minima of Lemma 5.12 are IsLeast (attained), and "equality iff $f = u_0$" reads as "iff $f$ is an eigenfunction for $E_0$", i.e. $f = c\,u_0$ with $|c| = 1$. $\min q \le E_0$ is $\exists x \in [a,b],\ q(x) \le E_0$. Norm convergence is $\operatorname{Re}\langle f - S_N, f - S_N\rangle \to 0$.
• Ruling out trivial readings. The resolvent is only considered with $W(z) \ne 0$ (Lean's $0^{-1} = 0$ would make it the zero operator). Scalar products are only applied to functions continuous on $[a,b]$, so no integral takes a junk value. Eigenfunctions must be nonzero on $[a,b]$. The expansion must hold in the weighted norm for every continuous $f$, which an orthonormal family that is merely orthonormal would not satisfy.

A complete development needs linear ODEs with a complex parameter and their analytic dependence on it, Green functions, an Arzelà–Ascoli argument in $C([a,b])$, and the spectral theorem for compact symmetric operators on an inner product space. The definitions RegularSL, SLOp, SLDomain, SLInner and SLWronskian are reusable for the oscillation and comparison theory (Theorems 5.17–5.25) in the rest of the chapter. Contributions connecting IsCompactOp to Mathlib's IsCompactOperator on the completion 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
• J. C. F. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 106–186. http://www.numdam.org/item/JMPA_1836_1_1__106_0/
• J. Liouville, Mémoire sur le développement des fonctions ou parties de fonctions en séries dont les divers termes sont assujettis à satisfaire à une même équation différentielle du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 253–265. http://www.numdam.org/item/JMPA_1836_1_1__253_0/
• E. Schmidt, Zur Theorie der linearen und nichtlinearen Integralgleichungen. I, Mathematische Annalen 63 (1907), 433–476. https://doi.org/10.1007/BF01449770

Motivation

Linear systems of ordinary differential equations $\dot x = A(t)x$ are the first case of the general theory in which solutions can be described structurally rather than merely shown to exist. They arise directly (circuits, mechanical vibrations, Hill's equation for the stability of periodic motions, the Mathieu equation for parametric resonance) and indirectly, as the linearization of a nonlinear system along an equilibrium or a periodic orbit. In the second role they decide stability: the linearized stability theorems of later chapters, the Poincaré map of a periodic orbit and the stable-manifold theory all reduce questions about nonlinear flows to questions about linear systems with constant or periodic coefficients.

For periodic coefficients the central structural result is due to Gaston Floquet (Sur les équations différentielles linéaires à coefficients périodiques, Annales scientifiques de l'École Normale Supérieure 12 (1883), 47–88, doi:10.24033/asens.220), preceded by G. W. Hill's 1877 work on the lunar perigee, which studied the same equation in the scalar second-order case. Liouville's formula for the Wronski determinant goes back to Abel (1829) and Liouville (1838). This mission follows Chapter 3 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012), in the author's preliminary version.

Setting

Fix $n \in \mathbb{N}$, an interval $I \subseteq \mathbb{R}$ and a continuous matrix function $A : I \to \mathbb{R}^{n\times n}$. A solution of the linear first-order system

$$\dot x(t) = A(t)\,x(t) \qquad (3.79)$$

on $I$ is a function $x$ with values in $\mathbb{R}^n$ that at every $t \in I$ has derivative $A(t)x(t)$ (one-sided at an endpoint of $I$). In Lean this is TeschlODE.Linear.IsSolution A I x.

The principal matrix solution $\Pi(t,t_0)$ is, for each $t_0 \in I$, the matrix function that solves the matrix initial value problem

$$\frac{d}{dt}\Pi(t,t_0) = A(t)\,\Pi(t,t_0), \qquad \Pi(t_0,t_0) = \mathbb{I}. \qquad (3.83)$$

Its columns are the solutions of (3.79) starting at the canonical basis vectors, and every solution is $x(t) = \Pi(t,t_0)x(t_0)$. In Lean the property is TeschlODE.Linear.IsPrincipalMatrixSolution A I Φ (the Lean name of $\Pi$ is Φ). The Wronski determinant of $n$ solutions $\varphi_1,\dots,\varphi_n$ is $W(t) = \det(\varphi_1(t),\dots,\varphi_n(t))$.

A system is periodic if $I = \mathbb{R}$ and $A(t+T) = A(t)$ for all $t$, for some $T > 0$ (3.117). Its monodromy matrix is $M(t_0) = \Pi(t_0+T, t_0)$ (3.119). A logarithm of a square matrix $M$ is any matrix $B$ with $\exp(B) = M$ (3.200), where $\exp$ is the matrix exponential.

Formalization targets

Goal: Floquet's theorem (Theorem 3.15)

Let $A \in C(\mathbb{R}, \mathbb{R}^{n\times n})$ be $T$-periodic with $T > 0$ and $\Pi$ its principal matrix solution. For every $t_0 \in \mathbb{R}$ there exist $Q(t_0) \in \mathbb{C}^{n\times n}$ and $P(\cdot,t_0) : \mathbb{R} \to \mathbb{C}^{n\times n}$ with

$$\Pi(t,t_0) = P(t,t_0)\,\exp\big((t-t_0)\,Q(t_0)\big), \qquad P(t+T,t_0) = P(t,t_0), \qquad P(t_0,t_0) = \mathbb{I}.$$

Milestones

In attack order:

1. Theorem 3.9 — for continuous $A$ on an interval $I$ the initial value problem $\dot x = A(t)x$, $x(t_0) = x_0$ has a unique solution, defined on all of $I$.
2. Theorem 3.10 — the solutions form an $n$-dimensional vector space, and a principal matrix solution exists with $x(t) = \Pi(t,t_0)x_0$.
3. Lemma 3.14 — for $T$-periodic $A$, $\Pi(t+T, t_0+T) = \Pi(t,t_0)$.
4. Lemma 3.11 (Liouville's formula) — $W(t) = W(t_0)\exp\big(\int_{t_0}^t \operatorname{tr} A(s)\,ds\big)$.
5. Lemma 3.34 — a complex matrix has a logarithm iff its determinant is nonzero; a real matrix whose real eigenvalues are all positive has a real logarithm; the square of an invertible real matrix has a real logarithm.
6. Theorem 3.12 (variation of constants) — the solution of $\dot x = A(t)x + g(t)$, $x(t_0) = x_0$, is $x(t) = \Pi(t,t_0)x_0 + \int_{t_0}^t \Pi(t,s)g(s)\,ds$.

Milestone 6 is not needed for the goal; it completes the linear theory of Section 3.4 on the same definitions and is the input to the perturbation results of Section 3.7.

Significance

Floquet's theorem reduces a periodic linear system to one with constant coefficients by a periodic change of variables. Its consequences in the book are the real version with doubled period (Corollary 3.16), the stability criterion in terms of Floquet multipliers (the eigenvalues of $M(t_0)$, Corollary 3.17), the reduction $y = P^{-1}x$ to $\dot y = Q y$ (Corollary 3.18), and the stability analysis of Hill's equation. Later in the book, the stability of a periodic orbit of a nonlinear system is read off from the Floquet multipliers of its linearization, via the Poincaré map.

All results of this mission have been proved for more than a century. What the mission adds is a machine-checked development: Mathlib has the matrix exponential (NormedSpace.exp, with Matrix.exp_add_of_commute), Picard–Lindelöf and Gronwall-type uniqueness for ODEs, but no principal matrix solution, no Liouville formula, no matrix logarithm and no Floquet theory. The two platform nodes named after Floquet's and Liouville's theorems are retired placeholders whose statement is True; no faithful formalization exists on the platform.

Difficulty

The obvious guess for the solution, $\exp\big(\int_{t_0}^t A(s)\,ds\big)x_0$, is wrong as soon as the values $A(t)$ do not commute, so neither Floquet's theorem nor the variation-of-constants formula can be obtained from the constant-coefficient theory by substitution. Floquet's theorem as stated is equivalent to the existence of a logarithm of the monodromy matrix: once $M(t_0) = \exp(TQ)$ is available, the periodicity of $P$ follows from Lemma 3.14. The existence of a matrix logarithm for every invertible complex matrix is the main missing piece of infrastructure; the logarithm is not unique and not continuous in the matrix, and a real invertible matrix need not have a real logarithm (a negative eigenvalue with a single Jordan block prevents it), which is why $Q(t_0)$ is complex. Liouville's formula, which gives $\det M(t_0) = \exp\big(\int_0^T \operatorname{tr} A\big) \neq 0$, needs the derivative of a determinant along a matrix solution.

Formalization scope

• Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ; $A(t)x$ is Matrix.mulVec. The goal and Lemma 3.34 use Matrix (Fin n) (Fin n) ℂ for $P$, $Q$ and the complex logarithm; $\Pi(t,t_0)$ is compared with $P\exp(\cdot)$ after coercing its entries to $\mathbb{C}$.
• An interval is a set $I$ with Set.OrdConnected I; continuity is ContinuousOn A I. Derivatives are HasDerivWithinAt … I t at every $t \in I$ (one-sided at endpoints in $I$); the matrix derivative in (3.83) is taken entrywise. In Section 3.6 (Lemma 3.14 and the goal) $I = \mathbb{R}$ and $A$ is Continuous.
• The principal matrix solution enters as a hypothesis IsPrincipalMatrixSolution A Set.univ Φ. Theorem 3.10 shows such a $\Phi$ exists and Theorem 3.9 shows it is unique on $I\times I$, so this hypothesis names the principal matrix solution, not an arbitrary function.
• Periodicity is 0 < T and ∀ t, A (t + T) = A t. The periodicity of $P$ is required with the same $T$ and for all $t$, together with $P(t_0,t_0) = \mathbb{I}$. Without the periodicity of $P$ the goal would be trivial ($Q = 0$, $P = \Pi$); with it, the goal carries the full content of the theorem.
• The matrix exponential is Mathlib's NormedSpace.exp. "Logarithm" means any $B$ with NormedSpace.exp B = M; no branch is fixed. In the third claim of Lemma 3.34 the hypothesis $\det A \ne 0$ is explicit: the book states it in the paragraph containing the lemma, and without it the claim fails at $A = 0$.
• "The solutions form an $n$-dimensional vector space" is expressed through restrictions to $I$: closure under linear combinations, $n$ solutions linearly independent on $I$, and every solution a combination of them on $I$.
• Needed infrastructure, reusable beyond this mission: existence and uniqueness for linear systems on arbitrary intervals, the principal matrix solution and its cocycle property $\Pi(t,t_1)\Pi(t_1,t_0) = \Pi(t,t_0)$, the derivative of $\det$ along a matrix solution, and the matrix logarithm (via the Jordan form or via the holomorphic functional calculus). Contributions of any of these as standalone lemmas 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, Chapter 3. https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf (published version: doi:10.1090/gsm/140).
• G. Floquet, Sur les équations différentielles linéaires à coefficients périodiques, Annales scientifiques de l'École Normale Supérieure 12 (1883), 47–88. doi:10.24033/asens.220
• W. J. Culver, On the existence and uniqueness of the real logarithm of a matrix, Proceedings of the AMS 17 (1966), 1146–1151. doi:10.1090/S0002-9939-1966-0202740-6