Dynamical Systems

Motivation

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

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

Setting

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

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

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

Formalization targets

Goal: Liouville's theorem (Theorem 8.10)

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).

Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).

Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.

Setting

A $p$ player normal form game gives player $\alpha$ an ordered finite strategy set $S^\alpha = \{0,\dots,n^\alpha - 1\}$ and a utility $u^\alpha$ on pure profiles. $\Sigma = \prod_\alpha \Delta S^\alpha$ is the set of mixed profiles, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\, s^\alpha = i} u^\alpha(s) \prod_{\beta \ne \alpha} x^\beta_{s^\beta}$.

The game is strictly supermodular if for all distinct players $\alpha \ne \beta$ and all profiles $s, \hat s$ with $s^\alpha > \hat s^\alpha$ and $s^{-\alpha} = \hat s^{-\alpha}$, the difference $u^\alpha(s) - u^\alpha(\hat s)$ is strictly increasing in $s^\beta = \hat s^\beta$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$, strictly positive, whose choice function $C^\alpha_i(\pi) = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$ is continuously differentiable. The perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$, and the perturbed best response dynamic is

$$(\mathrm P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

$RP(\mathrm P)$ is its set of rest points in $\Sigma$ and $CR(\mathrm P)$ its chain recurrent set.

In standard stochastic fictitious play the shocks $\varepsilon^\alpha_t$ have densities $f^\alpha$ and are independent over time and across players. From an arbitrary initial pure profile $\zeta_1$, each player at time $t+1$ plays the pure strategy maximizing $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where $Z_t = \frac1t \sum_{u \le t} \zeta_u$ is the vector of empirical frequencies.

The stochastic dominance coordinates are $(T^\alpha x^\alpha)_i = \sum_{j > i} x^\alpha_j \in \mathbb R^{n^\alpha - 1}$, the mass on strategies above $i$; $T x \le T y$ means each $y^\alpha$ stochastically dominates $x^\alpha$. In these coordinates (P) becomes a dynamic (T) on $T(\Sigma)$.

Formalization targets

Goal: Theorem 6.1(iv), unique rest point clause

For a strictly supermodular game with $p \ge 2$ players and shock densities as above, if $RP(\mathrm P) = \{x^*\}$ then

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1,$$

on every probability space, for every independent shock family with the given densities and every initial profile.

Milestones

• Lemma A.2, eq. (14), Lemma A.3 and eqs. (17)–(18): the order-theoretic and differential facts behind monotonicity.
• Theorem 5.1: $T^{-\alpha} y^{-\alpha} \ge T^{-\alpha} x^{-\alpha} \Rightarrow T^\alpha \tilde B^\alpha(y^{-\alpha}) \ge T^\alpha \tilde B^\alpha(x^{-\alpha})$.
• Theorem 5.2: there are rest points $\underline x, \bar x$ with $RP(\mathrm P) \subseteq [\underline x, \bar x]$.
• Proposition 5.3: (P) and (T) are linearly conjugate.
• Theorem 5.4: (T) is cooperative and irreducible.
• Corollary 5.5(i)–(ii): (P) is strongly monotone, and $CR(\mathrm P) \subseteq [\underline x, \bar x]$, so $CR(\mathrm P) = \{x^*\}$ when the rest point is unique.

Significance

The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.

The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.

Difficulty

The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space $T(\Sigma)$. The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that $x^*$ is globally asymptotically stable for (P) does not by itself give almost-sure convergence of $Z_t$. The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.

Formalization scope

Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every $n^\alpha \ge 1$. Mixed profiles live in the ambient space $\prod_\alpha \mathbb R^{n^\alpha}$ with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are $[0,\infty]$-valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are $C^1$. The process $Z_t$ is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.

A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process $Z_t$, on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.

A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size $1/t$. The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70 (2002), 2265–2294. https://doi.org/10.1111/1468-0262.00376 (formalized from the authors' manuscript of February 21, 2002)
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Repeated Games, Games and Economic Behavior 29 (1999), 36–72. https://doi.org/10.1006/game.1997.0636
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer (1999). https://doi.org/10.1007/BFb0096509
• M. Benaïm, Convergence with Probability One of Stochastic Approximation Algorithms Whose Average is Cooperative, Nonlinearity 13 (2000), 601–616. https://doi.org/10.1088/0951-7715/13/3/305
• H. L. Smith, Monotone Dynamical Systems, AMS Mathematical Surveys and Monographs 41 (1995). https://doi.org/10.1090/surv/041
• P. Milgrom and J. Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58 (1990), 1255–1277. https://doi.org/10.2307/2938316
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press (1998).

Motivation

Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).

Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part $G+G^T$ of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).

Setting

The network has $N$ vertices with states $x_i(t)\in\mathbb R^n$. A coupling matrix $G=(G_{ij})\in\mathbb R^{N\times N}$ has $G_{ij}\ge 0$ for $i\ne j$ ($G_{ij}>0$ means a connection from vertex $j$ to vertex $i$) and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. The network is strongly connected if any vertex can be reached from any other by a directed path; $G$ is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form $\begin{pmatrix}\tilde G_{11}&0\\\tilde G_{21}&\tilde G_{22}\end{pmatrix}$ with square diagonal blocks of sizes $m$ and $N-m$, $1\le m\le N-1$. The in-degree of vertex $i$ is $k_i^{\mathrm{in}}=\sum_{j\ne i}G_{ij}$.

Each vertex runs the dynamics $\dot x=f(x,t)$ for a continuously differentiable $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$. A reference trajectory $s$ solves $\dot s=f(s,t)$. With coupling strength $c$, inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and control gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\Gamma(x_i-s),\qquad i=1,\dots,N.$$

It is globally synchronized if $x_i(t)-s(t)\to0$ for every $i$, every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix $K$,

$$(x-y)^T\bigl(f(x,t)-f(y,t)\bigr)\le(x-y)^TK\Gamma(x-y)\qquad\forall x,y\in\mathbb R^n,\ t\ge0 .$$

For positive weights $\xi_1,\dots,\xi_N$ put $\Xi=\operatorname{diag}(\xi)$, $D=\operatorname{diag}(d)$ and $\widehat G=\tfrac12(\Xi G+G^T\Xi)$.

Formalization targets

Goal: Theorem 3.1 (p. 1402)

Let $f$ satisfy Assumption 1 with $\Gamma$ symmetric, let $G$ be a strongly connected coupling matrix, and let $\xi$ be positive with $\widehat G$ having zero row sums (the weights of Lemma 2.12). If

$$\Xi\otimes\frac{K\Gamma+\Gamma^TK^T}{2}+c\,\widehat G\otimes\frac{\Gamma+\Gamma^T}{2}-c\,(\Xi D)\otimes\frac{\Gamma+\Gamma^T}{2}<0,$$

then the controlled network is globally synchronized.

Milestones

The path to the goal follows the paper: Lemma 2.5 (irreducible $\iff$ strongly connected), Lemma 2.9 ($\rho(A)=\|A\|_\infty$ for nonnegative $A$ with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector $x$ with $G^Tx=0$), Lemma 2.12 (the weights $\Xi$), and the derivative estimate (3.4) for $V=\tfrac12\sum_i\xi_ie_i^Te_i$, $e_i=x_i-s$:

$$\dot V\le e^T\bigl[\Xi\otimes(K\Gamma)+c(\widehat G-\Xi D)\otimes\Gamma\bigr]e .$$

Companion results

Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions ($K\Gamma=\Gamma K$, $\theta=\lambda_{\max}(\tfrac{K+K^T}{2})\ge0$) with $\Gamma$ positive definite: Corollary 3.2 (the $N\times N$ condition $\theta\Xi+c(\widehat G-\Xi D)<0$ suffices), Corollary 3.3 (i) (an explicit coupling threshold $c>\lambda_{\max}(\theta\Xi)/|\lambda_{\max}(\widehat G-\Xi D)|$), and Corollary 3.4 (the necessary conditions $d_i>\theta/c-k_i^{\mathrm{in}}$ at pinned and $k_i^{\mathrm{in}}>\theta/c$ at unpinned vertices).

Significance

The criterion reduces global synchronization of an $nN$-dimensional nonlinear system to one linear matrix inequality in the data $(G,\Gamma,K,c,D)$, and the corollaries reduce it further to an $N\times N$ inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below $\theta/c$ must be controlled. Weighting by the left null vector of $G$ is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.

The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization $\widehat G$), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.

Difficulty

The obvious first idea, the unweighted Lyapunov function $\tfrac12\sum_ie_i^Te_i$, produces the symmetric part of $G$, which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of $G$, whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of $V$ along solutions on $[0,\infty)$, the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with $(A\otimes B)_{(i,a),(j,b)}=A_{ij}B_{ab}$; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of $0$ in $\mathbb R^n$, which does not depend on the norm. Derivatives are taken within $[0,\infty)$. Pinning is encoded by $d_i>0$ instead of the paper's reordering of the first $l$ vertices. "$M<0$" is positive definiteness of $-M$ (Mathlib PosDef, which includes symmetry); every matrix compared with $0$ is symmetric by construction. $\lambda_{\max}(A)$ of a symmetric matrix is the least $r$ with $v^TAv\le r\,v^Tv$ for all $v$; $\rho(A)$ is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.

Added hypotheses, each disclosed in the item: $\Gamma^T=\Gamma$ in Theorem 3.1 and (3.4), because the printed theorem allows any $\Gamma$ and is then false (a directed 3-cycle with $\Gamma=\begin{pmatrix}1&3\\-3&1\end{pmatrix}$ satisfies (3.2) but its error grows); $c>0$ in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); $N\ge1$ in Lemma 2.10. The weights $\Xi$ are not arbitrary: Theorem 3.1 and the corollaries require $\widehat G$ to have zero row sums, which for a coupling matrix is equivalent to $G^T\xi=0$. Assuming the derivative bound (3.4), negative definiteness of $\widehat G-\Xi D$ or decay of $V$ in the goal would trivialize it and is excluded.

The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54 (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• J. Zhou, J. Lu, J. Lü, Pinning adaptive synchronization of a general complex dynamical network, Automatica 44 (2008), 996–1003. https://doi.org/10.1016/j.automatica.2007.08.016
• W. Yu, G. Chen, J. Lü, On pinning synchronization of complex dynamical networks, Automatica 45 (2009), 429–435. https://doi.org/10.1016/j.automatica.2008.07.016
• Q. Song, J. Cao, On pinning synchronization of directed and undirected complex dynamical networks, IEEE Trans. Circuits Syst. I 57 (2010), 672–680. https://doi.org/10.1109/TCSI.2009.2024971
• R. Olfati-Saber, R. M. Murray, Consensus problems in networks of agents with switching topology and time-delays, IEEE Trans. Automat. Control 49 (2004), 1520–1533. https://doi.org/10.1109/TAC.2004.834113
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

Motivation

A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities $\varphi_i(x)=r_ix+t_i$, chosen with probabilities $p_i$. Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of $\sum_j\pm\lambda^j$, are the classical example. When the pieces $\varphi_i(K)$ are well separated, the dimension is given by the entropy-to-Lyapunov formula $H(p)/\chi$. When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals $\min\{1,h_{RW}/\chi\}$, where $h_{RW}$ is the entropy rate of the random walk on composed maps.

This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1946–1981 — Moran (Proc. Camb. Phil. Soc. 1946) and Hutchinson (Indiana 1981) give the similarity-dimension formula under separation and the invariant-measure construction.
• 1939–1996 — Erdős proves singularity of Bernoulli convolutions at reciprocal Pisot parameters (AJM 1939); Garsia introduces the entropy rate (Pacific J. Math. 1963); Solomyak proves a.e. absolute continuity (Annals 1995).
• 2009 — Feng and Hu prove exact dimensionality of self-similar measures without separation (CPAM 2009).
• 2014 — Hochman shows a dimension drop forces superexponential concentration of cylinders (Annals 2014).
• 2019 — Breuillard–Varjú (Ann. Probab. 2019) and Varjú's full dimension for transcendental parameters (Annals 2019).
• 2021 — Baker and Bárány–Käenmäki construct systems without exact overlaps whose cylinders approach superexponentially (Adv. Math. 2021, Adv. Math. 2021).
• 2022–2025 — Rapaport proves the no-exact-overlap formula for algebraic ratios (Ann. Sci. ENS 2022); Rapaport–Varjú treat homogeneous three-map systems (Duke 2024); Feng–Feng treat algebraic translations (J. LMS 2025).
• 2026 — Varjú's survey states the entropy-rate conjecture (Conjecture 3, arXiv:2509.22042).
• September 2026 — The OpenAI preprint claims the conjecture in full (Theorem 1.1, p. 2).

Setting

Let $\Lambda$ be a finite nonempty alphabet and $\varphi_i(x)=r_ix+t_i$ with $0<|r_i|<1$, $t_i\in\mathbb R$; different symbols may give the same map, and ratios may be negative and unequal. Let $p=(p_i)$ be a probability vector with all $p_i>0$. The self-similar measure $\mu$ is the Borel probability measure with

$$\mu=\sum_{i\in\Lambda}p_i\,(\varphi_i)_*\mu .$$

For a word $w=i_1\cdots i_n$ let $\varphi_w=\varphi_{i_1}\circ\cdots\circ\varphi_{i_n}$, and let $G_n$ be the random affine map $\varphi_w$ when the letters are independent with law $p$. With logarithms in base $2$,

$$h_{RW}=\inf_{n\ge1}\frac{H(G_n)}{n},\qquad \chi=-\sum_ip_i\log|r_i|>0,$$

where $H$ is Shannon entropy of the distribution of the map $G_n$ (coinciding words are merged). The lower Hausdorff dimension of $\mu$ is $\dim_H\mu=\inf\{\dim_HE: E\ \text{Borel},\ \mu(E)>0\}$. The system has no exact overlaps if distinct words of the same length give distinct maps.

Formalization targets

Milestone: Corollary 6.3 (p. 20) — dimension of the attractor

If there are no exact overlaps, the attractor $K=\{\lim_n\varphi_{\omega_1}\circ\cdots\circ\varphi_{\omega_n}(0)\}$ is compact and nonempty, the equation $\sum_i|r_i|^s=1$ has a unique solution $s_*\ge0$, and $\dim_HK=\min\{1,s_*\}$.

Milestone: Corollary 6.4 (p. 20) — homogeneous systems

If $r_i=\lambda\in(0,1)$ for all $i$ and there are no exact overlaps, then $\dim_H\mu=\min\{1,H(p)/\log(1/\lambda)\}$.

Goal: Theorem 1.1 (p. 2)

For every such family and every strictly positive probability vector $p$,

$$\dim_H\mu=\min\Bigl\{1,\ \frac{h_{RW}}{\chi}\Bigr\}.$$

No separation assumption is made; exact overlaps and repeated generators are allowed.

Significance

The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below $\min\{1,H(p)/\chi\}$ is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.

Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.

Difficulty

Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).

Formalization scope

• A System ι over a nonempty Fintype ι carries ratio, offset, weight with $0<|r_i|<1$, $p_i>0$, $\sum p_i=1$. SelfSimilar S μ is the equation $\mu=\sum_i p_i\,(\varphi_i)_*\mu$ for a probability measure $\mu$ on $\mathbb R$.
• wordAffine composes maps as $\varphi_{i}\circ\varphi_w$ and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of $G_n$; entropyRate is the sInf over $n\ge1$ of $H(G_n)/n$; lyapunov is base-2.
• lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable $E$ with $\mu(E)>0$; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).
• NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are $0$.
• The attractor milestone uses its own coding map codingPoint and word functions, equivalent to the definitions above.

Selected references

• OpenAI, The entropy-rate dimension formula for self-similar measures on the line, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf
• P. P. Varjú, Entropy rates in the dimension theory of self-similar measures, arXiv:2509.22042 (2026). https://arxiv.org/abs/2509.22042v2
• J. E. Hutchinson, Fractals and self-similarity, Indiana Univ. Math. J. 30 (1981). https://doi.org/10.1512/iumj.1981.30.30055
• D.-J. Feng, H. Hu, Dimension theory of iterated function systems, Comm. Pure Appl. Math. (2009). https://doi.org/10.1002/cpa.20276
• M. Hochman, On self-similar sets with overlaps and inverse theorems for entropy, Ann. of Math. 180 (2014). https://doi.org/10.4007/annals.2014.180.2.7
• P. P. Varjú, On the dimension of Bernoulli convolutions for all transcendental parameters, Ann. of Math. 189 (2019). https://doi.org/10.4007/annals.2019.189.3.9
• E. Breuillard, P. P. Varjú, On the dimension of Bernoulli convolutions, Ann. Probab. (2019). https://doi.org/10.1214/18-AOP1324
• A. Rapaport, Proof of the exact overlaps conjecture for systems with algebraic contractions, Ann. Sci. ENS (2022). https://doi.org/10.24033/asens.2518
• A. Rapaport, P. P. Varjú, Self-similar measures associated to a homogeneous system of three maps, Duke Math. J. (2024). https://doi.org/10.1215/00127094-2023-0019
• S. Baker, Iterated function systems with super-exponentially close cylinders, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107548
• B. Bárány, A. Käenmäki, Super-exponential condensation without exact overlaps, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107549
• B. Solomyak, On the random series Σ±λ^n (an Erdős problem), Ann. of Math. (1995). https://doi.org/10.2307/2118556

Motivation

A cellular automaton over a group $G$ with a finite alphabet $A$ is a map on configurations $x : G \to A$ that updates every cell by the same finite local rule, read off from a finite neighbourhood of that cell. Cellular automata over $\mathbb{Z}^d$ go back to von Neumann and Ulam and are a standard model in symbolic dynamics; replacing $\mathbb{Z}^d$ by an arbitrary group links the theory to geometric group theory.

In 1973 Gottschalk asked which groups $G$ have the property that every injective cellular automaton over $G$ is automatically surjective, and called such groups surjunctive. For a finite group this is the pigeonhole principle, since $A^G$ is then a finite set. For infinite groups the configuration space is an uncountable compact space and the pigeonhole principle is no longer available. Gottschalk's surjunctivity conjecture states that every group is surjunctive. It is open.

Timeline

• 1962–1963 — Moore and Myhill prove the Garden of Eden theorem for $\mathbb{Z}^2$ (and, in the same way, $\mathbb{Z}^d$): a cellular automaton is surjective if and only if it is pre-injective. In particular $\mathbb{Z}^d$ is surjunctive.
• 1969 — Hedlund (crediting Curtis and Lyndon) characterises cellular automata over $\mathbb{Z}$ as the continuous shift-commuting self-maps of $A^{\mathbb{Z}}$ (the Curtis–Hedlund–Lyndon theorem); the characterisation extends to every group.
• 1973 — Gottschalk introduces surjunctivity and states the conjecture; he records Lawton's result that residually finite groups are surjunctive.
• 1999 — Ceccherini-Silberstein, Machì and Scarabotti prove the Garden of Eden theorem for amenable groups, which implies that amenable groups are surjunctive.
• 1999–2000 — Gromov introduces what Weiss names sofic groups, and both show that sofic groups are surjunctive. Sofic groups include all residually finite groups and all amenable groups.
• Today — no group is known to be non-sofic, and no group is known to be non-surjunctive.

Setting

Fix a group $G$ and a finite nonempty set $A$ (the alphabet). A configuration is a function $x : G \to A$; the set of configurations is $A^G$. It carries the product topology, where $A$ has the discrete topology; this makes $A^G$ compact.

The left shift of $x$ by $g \in G$ is the configuration

$$(g \cdot x)(h) = x(g^{-1}h), \qquad h \in G,$$

written shift G g x in the Lean development. A map $\tau : A^G \to A^G$ is shift-equivariant (IsShiftEquivariant) if $\tau(g\cdot x) = g\cdot\tau(x)$ for all $g$ and $x$.

The group $G$ is surjunctive (IsSurjunctive) if, for every finite nonempty alphabet $A$, every map $\tau : A^G \to A^G$ that is continuous, shift-equivariant and injective is also surjective.

A map $\tau$ is a cellular automaton (IsCellularAutomaton) if there are a finite memory set $S \subseteq G$ and a local rule $\mu : A^S \to A$ with

$$\tau(x)(g) = \mu\big(s \mapsto x(gs)\big) \qquad \text{for all } x \in A^G,\ g \in G.$$

Three classes of groups appear in the milestones:

1. $G$ is residually finite (IsResiduallyFinite) if every $g \neq 1$ lies outside some normal subgroup of finite index.
2. $G$ is amenable if there is a finitely additive, left-invariant probability measure defined on all subsets of $G$ (the existing platform definition Garrido.IsAmenable).
3. $G$ is sofic (IsSofic) if for every finite $K \subseteq G$ and every $\varepsilon > 0$ there are a finite nonempty set $X$ and a map $\sigma : G \to \mathrm{Sym}(X)$ such that $\sigma_{gh}(x) = \sigma_g(\sigma_h(x))$ for at least a $(1-\varepsilon)$ fraction of the points $x \in X$ whenever $g, h \in K$, and $\sigma_g(x) \neq x$ for at least a $(1-\varepsilon)$ fraction of the points whenever $g \in K \setminus \{1\}$.

Formalization targets

Goal: Gottschalk's conjecture

$$\forall\, G \text{ group}: \quad G \text{ is surjunctive.}$$

Milestones

1. Curtis–Hedlund–Lyndon: for finite $A$, a map $\tau : A^G \to A^G$ is continuous and shift-equivariant if and only if it is a cellular automaton.
2. Subgroups: every subgroup of a surjunctive group is surjunctive.
3. Local character: if every finitely generated subgroup of $G$ is surjunctive, then $G$ is surjunctive.
4. Finite groups are surjunctive.
5. Residually finite groups are surjunctive (Lawton).
6. Amenable groups are surjunctive (Ceccherini-Silberstein–Machì–Scarabotti).
7. Sofic groups are surjunctive (Gromov; Weiss).

Significance

The result itself. A positive answer would make the implication "injective $\Rightarrow$ surjective" for cellular automata hold unconditionally, extending the pigeonhole principle from finite sets to all shift spaces $A^G$. Surjunctivity is also tied to Kaplansky's direct finiteness conjecture: for a surjunctive group $G$ and any finite field $K$, the group ring $K[G]$ is directly finite ($ab = 1 \Rightarrow ba = 1$). A counterexample would be the first known non-sofic group, since sofic groups are surjunctive.

Formalizing it. Milestones 4–7 are proved results in the literature; milestones 1–3 are standard facts of the theory. At the time of writing, none of milestones 1–3 and 5–7 is known to exist as a machine-checked proof on this platform. Formalizing them requires building the basic theory of cellular automata over groups (memory sets, local rules, induced automata on subgroups), which can be reused by other work in symbolic dynamics. The goal theorem itself is open.

Difficulty

For infinite $G$ the space $A^G$ is infinite, so no counting argument applies directly. All known proofs approximate $G$ by finite objects: finite quotients (residually finite case), Følner sets with an entropy count (amenable case), or approximate finite permutation models (sofic case). No such approximation is known to exist for every group, and it is not known whether every group is sofic. A proof of the full conjecture therefore needs either a proof that every group is sofic or an argument that does not go through finite approximations.

Formalization scope

• Groups $G$ and alphabets $A$ live in Type (universe $0$). Alphabets are finite (Fintype) and nonempty; their topology is an arbitrary topology assumed to be discrete, and $A^G$ carries Lean's product topology.
• The shift is a plain function shift, not a MulAction instance, to avoid a clash with Mathlib's pointwise action on function types.
• Amenability is taken from the existing platform definition Garrido.IsAmenable (finitely additive invariant probability measure on all subsets). Residual finiteness and soficity are defined in GottschalkSurjunctivity_Defs.
• Soficity is stated with a normalised count of points; the conditions are required for every $\varepsilon > 0$, so small $\varepsilon$ is where the content lies.
• Surjunctivity is not trivialised by the nonemptiness assumption: for a nonempty group and a nonempty alphabet, $A^G$ is nonempty and, when $G$ is infinite, uncountable.

Contributions welcome: the Curtis–Hedlund–Lyndon theorem, restriction and induction of cellular automata along subgroups, and the residually finite case are natural first steps.

Selected references

• W. H. Gottschalk, Some general dynamical notions, Recent Advances in Topological Dynamics, Lecture Notes in Math. 318, Springer, 1973, pp. 120–125. https://doi.org/10.1007/BFb0061728
• G. A. Hedlund, Endomorphisms and automorphisms of the shift dynamical system, Math. Systems Theory 3 (1969), 320–375. https://doi.org/10.1007/BF01691062
• T. Ceccherini-Silberstein, A. Machì, F. Scarabotti, Amenable groups and cellular automata, Ann. Inst. Fourier 49 (1999), 673–685. https://doi.org/10.5802/aif.1686
• M. Gromov, Endomorphisms of symbolic algebraic varieties, J. Eur. Math. Soc. 1 (1999), 109–197. https://doi.org/10.1007/PL00011162
• B. Weiss, Sofic groups and dynamical systems, Sankhyā Ser. A 62 (2000), 350–359.
• T. Ceccherini-Silberstein, M. Coornaert, Cellular Automata and Groups, Springer Monographs in Mathematics, 2010. https://doi.org/10.1007/978-3-642-14034-1
• Wikipedia, Surjunctive group. https://en.wikipedia.org/wiki/Surjunctive_group

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