Dynamical Systems

Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.

Motivation

The iteration of a rational map $f:\hat{\mathbb C}\to\hat{\mathbb C}$ of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.

Timeline of the results formalized here:

• 1912–1927, Montel. Families of holomorphic maps omitting three values are normal (Milnor, Theorem 3.7).
• 1918–1920, Fatou and Julia. Definition of the Fatou and Julia sets; the Julia set of a map of degree $d\ge2$ is nonempty and equals the closure of the repelling periodic points (Milnor, Lemma 4.8 and Theorem 14.1).
• 1920s–1942. Fatou classified the possible dynamics on an invariant Fatou component; Siegel (1942) showed that Siegel disks exist, and Herman (1979) constructed Herman rings. Together these give the four cases of Milnor's Theorem 16.1.
• 1985, Sullivan. Every Fatou component is eventually periodic (Sullivan, Quasiconformal homeomorphisms and dynamics I, Ann. of Math. 122 (1985); Milnor, Theorem 16.4).

Setting

The Riemann sphere is $\hat{\mathbb C}=\mathbb C\cup\{\infty\}$, the one-point compactification of $\mathbb C$, with the two coordinates $z$ (near finite points) and $1/z$ (near $\infty$). A rational map is $f=p/q$ with $p,q$ coprime complex polynomials, $q\neq0$; it acts on $\hat{\mathbb C}$ in the usual way, and its degree is $d=\max(\deg p,\deg q)$. Write $f^{\circ n}$ for the $n$-th iterate.

A family of maps from an open set to $\hat{\mathbb C}$ is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set $F(f)$ is the set of points having a neighbourhood on which the iterates $\{f^{\circ n}\}$ form a normal family; the Julia set is its complement $J(f)=\hat{\mathbb C}\setminus F(f)$. A Fatou component is a connected component of $F(f)$. A periodic point $z_0=f^{\circ m}(z_0)$ of minimal period $m$ has multiplier $\lambda=(f^{\circ m})'(z_0)$, computed in a local coordinate; it is repelling if $|\lambda|>1$ and attracting if $|\lambda|<1$.

A Fatou component $U$ with $f(U)=U$ is a Siegel disk (resp. Herman ring) if $f|_U$ is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus $\{1<|w|<r\}$).

Formalization targets

Goal: no wandering domains (Theorem 16.4)

For a rational map $f$ of degree $d\ge2$ and every Fatou component $U$ there are $n\ge0$, $p\ge1$ with

$$f^{\circ p}\bigl(f^{\circ n}(U)\bigr)=f^{\circ n}(U).$$

Milestones

1. Lemma 2.5: $\hat{\mathbb C}\setminus\{0,1,\infty\}$ is covered holomorphically by the unit disk.
2. Corollary 3.3 (case $\mathbb D\to\mathbb C\setminus\{0,1\}$): holomorphic maps between hyperbolic surfaces form a normal family.
3. Lemma 3.5 (case $\mathbb C\setminus\{0,1\}\subset\hat{\mathbb C}$).
4. Theorem 3.7 (Montel): holomorphic maps from a domain to $\hat{\mathbb C}$ omitting three values form a normal family.
5. Lemma 4.3: $z\in J(f)\iff f(z)\in J(f)$.
6. Lemma 4.4: $J(f^{\circ k})=J(f)$ for $k>0$.
7. Lemma 4.8: $J(f)\neq\emptyset$ when $d\ge2$.
8. Theorem 14.1: $J(f)=\overline{\{\text{repelling periodic points}\}}$ when $d\ge2$.
9. Theorem 16.1: an invariant Fatou component is an attracting basin, a parabolic basin, a Siegel disk or a Herman ring.

Significance

The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of $J$, density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).

Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.

Difficulty

The early milestones need the uniformization-type input that $\mathbb C\setminus\{0,1\}$ is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of $J$ that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of $f$, contradicting the finite dimensionality of the space of rational maps of degree $d$. The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.

Formalization scope

All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.

• $\hat{\mathbb C}$ is OnePoint ℂ; a rational map is a structure of coprime polynomials $p,q$ with $q\ne0$, acting on OnePoint ℂ via RationalMap.toFun; the degree is $\max(\deg p,\deg q)$.
• Holomorphy of a map into $\hat{\mathbb C}$ on an open $U\subseteq\mathbb C$ is continuity plus complex differentiability in the charts $z$ and $1/z$ (IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of $\hat{\mathbb C}$.
• Multipliers are derivatives of $f^{\circ m}$ in the standard chart at the periodic point, $m$ the minimal period.
• Montel's theorem is stated for a domain $U\subseteq\mathbb C$ rather than an arbitrary Riemann surface (normality is local, Milnor Problem 3-e); Lemma 2.5, Corollary 3.3 and Lemma 3.5 are linked in the special cases used for Montel's theorem.
• The degree hypotheses are Milnor's: $d\ge1$ (nonconstant) in §4 Lemmas 4.3–4.4, $d\ge2$ elsewhere. Without $d\ge2$ several statements are false (e.g. $J(z\mapsto 2z)=\emptyset$), so the hypothesis must not be dropped.

Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of $\mathbb C\setminus\{0,1\}$, the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.

Selected references

• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. https://doi.org/10.1515/9781400835539
• D. Sullivan, Quasiconformal homeomorphisms and dynamics I. Solution of the Fatou–Julia problem on wandering domains, Ann. of Math. 122 (1985), 401–418. https://doi.org/10.2307/1971308
• L. Carleson and T. W. Gamelin, Complex Dynamics, Universitext, Springer, 1993. https://doi.org/10.1007/978-1-4612-4364-9
• P. Montel, Leçons sur les familles normales de fonctions analytiques et leurs applications, Gauthier-Villars, Paris, 1927.

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

Motivation

Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.

Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.

Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some $p$ player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.

Setting

A $p$ player game has finite strategy sets $S^\alpha = \{0,\dots,n^\alpha-1\}$ and utilities $u^\alpha : S \to \mathbb R$ on pure profiles $S = \prod_\beta S^\beta$. The game is a potential game if $u^\alpha(s) = u^\beta(s)$ for all players and all profiles. Mixed profiles form $\Sigma = \prod_\alpha \Delta S^\alpha$, 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}$.

Player $\alpha$'s payoffs are perturbed by a random vector $\varepsilon^\alpha$ with a strictly positive density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function is $C^\alpha_i(\pi) = P(\arg\max_j \pi_j + \varepsilon^\alpha_j = i)$, assumed continuously differentiable, and the perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$.

In standard stochastic fictitious play, shocks $\varepsilon^\alpha_t$ are independent over time and across players. From an arbitrary initial pure profile, at time $t+1$ each player plays a maximizer of $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t\sum_{u=1}^t \zeta_u .$$

The mean dynamic of this process is the perturbed best response dynamic

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

A rest point $x^*$ of (P) is hyperbolic if every eigenvalue of $DF(x^*)$ restricted to the tangent space $\prod_\alpha \mathbb R^{n^\alpha}_0$ of $\Sigma$ has nonzero real part, and linearly stable if every such eigenvalue has negative real part. $RP(P)$ and $LS(P)$ denote the rest points and the linearly stable rest points.

By Theorem 2.1 of the paper, $C^\alpha(\pi) = \arg\max_{y\in\operatorname{int}\Delta}(y\cdot\pi - V^\alpha(y))$ for an admissible deterministic perturbation $V^\alpha$, so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces $C^\alpha$.

Formalization targets

Goal: Theorem 6.1(iii)

For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:

1. if the shocks are smooth enough that the $V^\alpha$ are $C^N$, $N = \sum_\alpha(n^\alpha-1)$, then

$$P\big(\omega(Z_t)\text{ is a connected subset of } RP(P)\big) = 1;$$

2. if every rest point of (P) is hyperbolic and the field of (P) is $C^2$, then

$$P\Big(\lim_{t\to\infty} Z_t \text{ exists and lies in } LS(P)\Big) = 1.$$

Milestones

In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function $\Pi(x) = \sum_s u^1(s)\prod_\alpha x^\alpha_{s^\alpha} - \sum_\alpha V^\alpha(x^\alpha)$ is a strict Lyapunov function for (PV)), the identification of the critical points of $\Pi$ with the rest points of (PV), Proposition 4.2 ($CR(PV) = RP(PV)$ under $C^N$ smoothness), Proposition 4.3 (under hyperbolicity $RP(PV)$ is finite and equals $CR(PV)$), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).

Significance

The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential $\Pi$. Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.

Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.

Difficulty

The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a $C^N$ function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process $Z_t$.

Formalization scope

Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process $Z_t$ is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of $V^\alpha$ are those of $V^\alpha$ composed with the projection onto the plane $\sum_i y_i = 1$. Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of $\Sigma$. Solutions of a dynamic are differentiable curves on $[0,\infty)$ that stay in $\Sigma$, and chain recurrence uses $\varepsilon$-chains with times $t_i \ge 1$.

A formalization about the ODE (P) in place of the process $Z_t$, a fixed noise law such as logit, or convergence to $RP(P)$ in place of $LS(P)$ would prove a different and weaker statement. These are excluded.

Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of $C^1$ vector fields on compact sets, Sard's theorem for real-valued $C^N$ functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• R. Pemantle, Nonconvergence to Unstable Points in Urn Models and Stochastic Approximations, Annals of Probability 18(2), 698–712, 1990. https://doi.org/10.1214/aop/1176990853
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

Structural stability asks when the qualitative behaviour of a dynamical system survives small perturbations. A diffeomorphism $f$ of a closed manifold is structurally stable if every diffeomorphism $g$ close enough to $f$ is topologically conjugate to $f$: some homeomorphism $h$ of the manifold satisfies $h\circ f=g\circ h$, so that $h$ carries orbits of $f$ onto orbits of $g$. Systems that model physical phenomena are only known up to small errors, which is the original reason for interest in this notion (Andronov–Pontryagin, 1937).

In the 1960s Smale introduced Axiom A, a uniform-hyperbolicity condition on the nonwandering set, and showed that it yields a detailed description of the dynamics (spectral decomposition, symbolic dynamics). Palis and Smale conjectured that structural stability forces this hyperbolic structure. The conjecture appears on the Open Problem Garden as the $C^r$ Stability Conjecture (openproblemgarden.org/op/c_r_stability_conjecture, rated Outstanding): any $C^r$ structurally stable diffeomorphism is hyperbolic. The same page describes the higher-regularity case as one of the most important and difficult problems in dynamical systems.

Timeline.

• 1967 — D. V. Anosov proves that Anosov diffeomorphisms (the whole manifold is a hyperbolic set) are structurally stable (Proc. Steklov Inst. Math. 90).
• 1970 — J. Palis and S. Smale prove that Morse–Smale diffeomorphisms are structurally stable and state the stability conjecture: $f$ is structurally stable if and only if $f$ satisfies Axiom A and the strong transversality condition (Global Analysis, Proc. Sympos. Pure Math. 14, AMS).
• 1971 — J. Robbin proves the "if" direction for $C^2$ diffeomorphisms (Ann. of Math. 94); J. Franks obtains necessary conditions for $C^1$ stability, including hyperbolicity of periodic points (Trans. Amer. Math. Soc. 158).
• 1976 — C. Robinson proves the "if" direction for $C^1$ diffeomorphisms (J. Differential Equations 22).
• 1988 — R. Mañé proves the "only if" direction in the $C^1$ topology: a $C^1$ structurally stable diffeomorphism satisfies Axiom A (Publ. Math. IHÉS 66). In the same volume J. Palis derives the $C^1$ $\Omega$-stability conjecture.
• 1997 — S. Hayashi proves the analogous $C^1$ statements for flows (Ann. of Math. 145).

For every $r\ge 2$ the "only if" direction remains open.

Setting

Let $M$ be a closed manifold: a compact Hausdorff smooth manifold without boundary, of dimension $n$. For an integer $r\ge 1$, $\mathrm{Diff}^r(M)$ is the set of $C^r$ diffeomorphisms $f\colon M\to M$, with the $C^r$ topology: $g$ is close to $f$ when, in finitely many charts and on compact sets, $g$ and its derivatives of order $\le r$ are uniformly close to those of $f$.

• A point $x$ is nonwandering for $f$ if for every neighbourhood $U$ of $x$ there is $k\ge 1$ with $f^k(U)\cap U\neq\emptyset$. The nonwandering points form the compact invariant set $\Omega(f)$. Every periodic point lies in $\Omega(f)$.
• A compact set $\Lambda$ with $f(\Lambda)=\Lambda$ is hyperbolic if, for a continuous Riemannian metric, each tangent space $T_xM$, $x\in\Lambda$, splits as $E^s(x)\oplus E^u(x)$, the splitting is carried to itself by $Df$, and there are $C>0$ and $0<\lambda<1$ with

$$\|Df^k_x v\|\le C\lambda^k\|v\|\ (v\in E^s(x)),\qquad \|Df^{-k}_x v\|\le C\lambda^k\|v\|\ (v\in E^u(x)),\qquad k\ge 0 .$$

• $f$ satisfies Axiom A if $\Omega(f)$ is hyperbolic and the periodic points of $f$ are dense in $\Omega(f)$. $f$ is Anosov if $M$ itself is hyperbolic.
• $f$ is $C^r$ structurally stable if some $C^r$ neighbourhood of $f$ consists of diffeomorphisms topologically conjugate to $f$. It is $C^r$ $\Omega$-stable if for all $g$ in some $C^r$ neighbourhood, $f|_{\Omega(f)}$ and $g|_{\Omega(g)}$ are topologically conjugate.

Formalization targets

Goal: the $C^r$ stability conjecture

For every closed manifold $M$, every $r\ge 1$ and every $f\in\mathrm{Diff}^r(M)$,

$$f \text{ is } C^r \text{ structurally stable} \;\Longrightarrow\; f \text{ satisfies Axiom A}.$$

The case $r=1$ is Mañé's theorem; the cases $r\ge 2$ are open.

Milestones

1. Franks (1971). A $C^1$ structurally stable diffeomorphism has only hyperbolic periodic points.
2. Consequence of Pugh's closing lemma. For a $C^1$ structurally stable $f$, $\overline{\mathrm{Per}(f)}=\Omega(f)$.
3. Mañé (1988). The goal for $r=1$.
4. Palis (1988). A $C^1$ $\Omega$-stable diffeomorphism satisfies Axiom A.
5. Anosov (1967). For every $r\ge1$, an Anosov $C^r$ diffeomorphism is $C^r$ structurally stable.

Significance

The result. A positive answer would give a dynamical characterization of structural stability in every regularity: together with the theorems of Robbin and Robinson (Axiom A plus strong transversality implies stability), it would show that structurally stable diffeomorphisms are exactly the hyperbolic ones with transverse stable and unstable manifolds. Every structurally stable system would then inherit Smale's spectral decomposition and its symbolic models. In the $C^1$ topology this picture is complete (Mañé); in higher regularity it is not known whether a structurally stable system can fail to be hyperbolic.

Formalizing it. The mission produces a common Lean vocabulary for hyperbolic sets, Axiom A, and structural and $\Omega$-stability of diffeomorphisms of closed manifolds, compatible with the existing $C^r$ topology and nonwandering-set definitions on the platform. The proved cases (Anosov, Franks, Mañé, Palis) are milestones whose formal proofs would be new contributions; the goal itself is open for $r\ge 2$.

Difficulty

The known $C^1$ proof rests on perturbation tools that work only in the $C^1$ topology: Franks' lemma (realizing any small change of the derivative along a periodic orbit by a $C^1$-small perturbation), Pugh's closing lemma and Mañé's ergodic closing lemma. In the $C^r$ topology, $r\ge 2$, a perturbation that changes the derivative by a fixed amount on a small ball has large higher derivatives, so these local constructions are not $C^r$-small; Gutierrez's examples on the torus show that the local perturbation schemes used for the $C^1$ closing lemma cannot work in the $C^2$ topology. Whether periodic points are even dense in $\Omega(f)$ for a $C^r$ structurally stable $f$ is a case of the $C^r$ closing problem, itself open.

Formalization scope

• $M$ is a type with [TopologicalSpace M] [T2Space M] [CompactSpace M], a ChartedSpace structure over EuclideanSpace ℝ (Fin n) and IsManifold (𝓡 n) ∞ M (smooth, no boundary). $\mathrm{Diff}^r(M)$ is ClosingLemma.Diff n M r with the weak $C^r$ topology ClosingLemma.crTopology r (published definition ClosingLemma_DiffeoCrTopology); on compact $M$ it coincides with the strong topology. $r$ is a natural number with $r\ge 1$; $r=\infty$ is not covered.
• $\Omega(f)$ is PughClosingLemma.nonwanderingSet (published definition PughClosingLemma_nonwandering).
• Hyperbolicity uses mfderiv and an arbitrary continuous Riemannian metric (Bundle.ContinuousRiemannianMetric on the tangent bundle); since $M$ is compact, the choice of metric only changes $C$. Continuity of the splitting is not assumed, being a consequence of the estimates. A periodic point is hyperbolic when its finite orbit is a hyperbolic set, which is equivalent to the eigenvalue condition.
• Axiom A requires density of periodic points in $\Omega(f)$ as a separate condition, following Smale's definition.
• Structural stability asks only for a conjugating homeomorphism, without requiring it to be close to the identity. The strong transversality part of the Palis–Smale conjecture is not part of the goal.
• Infrastructure needed: stable manifold theory for hyperbolic sets, shadowing, Franks' lemma and closing lemmas on manifolds. These are reusable beyond this mission, and contributions of them are welcome.

Selected references

• Open Problem Garden, $C^r$ Stability Conjecture, posted December 20, 2007. https://www.openproblemgarden.org/op/c_r_stability_conjecture
• D. V. Anosov, Geodesic flows on closed Riemannian manifolds with negative curvature, Proc. Steklov Inst. Math. 90, 1967.
• J. Palis, S. Smale, Structural stability theorems, Global Analysis, Proc. Sympos. Pure Math. 14, AMS, 1970.
• J. Robbin, A structural stability theorem, Ann. of Math. 94, 1971.
• J. Franks, Necessary conditions for stability of diffeomorphisms, Trans. Amer. Math. Soc. 158, 1971.
• C. Robinson, Structural stability of $C^1$ diffeomorphisms, J. Differential Equations 22, 1976.
• R. Mañé, A proof of the $C^1$ stability conjecture, Publ. Math. IHÉS 66, 1988.
• J. Palis, On the $C^1$ $\Omega$-stability conjecture, Publ. Math. IHÉS 66, 1988.
• S. Hayashi, Connecting invariant manifolds and the solution of the $C^1$ stability and $\Omega$-stability conjectures for flows, Ann. of Math. 145, 1997.
• C. Pugh, An improved closing lemma and a general density theorem, Amer. J. Math. 89, 1967.

Motivation

Dynamic stochastic general equilibrium (DSGE) models are the standard framework used by central banks and fiscal authorities for policy analysis and forecasting (Wikipedia overview). The models used for monetary-policy analysis are built from three interrelated blocks — demand, supply and a monetary-policy rule — that jointly determine output, inflation and the nominal interest rate. The canonical small-scale instance is the three-equation New Keynesian model (Woodford 2003; Galí 2008; Clarida, Galí and Gertler 1999).

A basic question about such a model is whether it pins down a unique equilibrium path at all. If many bounded paths solve the model, the model makes no definite prediction and expectations can become self-fulfilling. The answer for the three-equation model is the Taylor principle: the interest-rate rule must respond to inflation strongly enough.

Timeline. Blanchard and Kahn (1980) gave the eigenvalue-counting criterion for existence and uniqueness of bounded solutions of linear rational-expectations models. Kydland and Prescott (1982) started the real-business-cycle/DSGE programme. Rotemberg and Woodford (1997) introduced the New Keynesian DSGE framework. Bullard and Mitra (2002) derived the explicit determinacy condition $\kappa(\phi_\pi - 1) + (1-\beta)\phi_y > 0$ for the model with a contemporaneous Taylor rule, presented in textbook form by Galí (2008, Ch. 3).

Setting

Time is discrete, $t = 0, 1, 2, \dots$. All variables are deviations from the zero-inflation steady state: $y_t$ is the output gap, $\pi_t$ inflation, and $i_t$ the nominal interest rate. The parameters are $\sigma > 0$ (inverse elasticity of intertemporal substitution), $\beta \in (0,1)$ (discount factor), $\kappa > 0$ (slope of the Phillips curve), and the policy coefficients $\phi_\pi, \phi_y \ge 0$.

A triple of real sequences $(y, \pi, i)$ is an equilibrium if for every $t$

$$\begin{aligned} y_t &= y_{t+1} - \tfrac{1}{\sigma}(i_t - \pi_{t+1}) && \text{(demand: dynamic IS curve)}\\ \pi_t &= \beta \pi_{t+1} + \kappa y_t && \text{(supply: New Keynesian Phillips curve)}\\ i_t &= \phi_\pi \pi_t + \phi_y y_t && \text{(monetary policy: Taylor rule).} \end{aligned}$$

The demand equation is the log-linearised consumption Euler equation, which equates marginal utility of consumption today with discounted marginal utility tomorrow. The model is determinate if the zero path is its only equilibrium in which $y$, $\pi$ and $i$ all stay bounded.

Formalization targets

Goal: the Taylor principle

For $\sigma > 0$, $0 < \beta < 1$, $\kappa > 0$, $\phi_\pi, \phi_y \ge 0$:

$$\text{the model is determinate} \iff \kappa(\phi_\pi - 1) + (1 - \beta)\phi_y > 0 .$$

Milestones

1. Consumption Euler equation. At an interior optimum of the two-period consumption–saving problem, $u'(c_0) = \beta(1+r)u'(c_1)$.
2. State-space form. For $\sigma, \beta \ne 0$, the model is equivalent to $(y_{t+1}, \pi_{t+1})^\top = M(y_t, \pi_t)^\top$ together with the Taylor rule, for an explicit $2\times2$ matrix $M$.
3. Equilibria are parametrised by initial conditions. Each $(y_0, \pi_0)$ determines exactly one equilibrium.
4. Schur–Cohn test. For real $T$ and $D > 0$, both roots of $z^2 - Tz + D$ have modulus $> 1$ iff $D > 1$ and $|T| < 1 + D$.
5. Blanchard–Kahn lemma. For a real square matrix $M$, the only bounded solution of $x_{t+1} = Mx_t$ is zero iff every complex eigenvalue of $M$ has modulus $> 1$.

Significance

The result itself. The Taylor principle is the standard criterion for whether an interest-rate rule yields a well-defined equilibrium in New Keynesian models, and it is the first property checked when a policy rule is proposed. The determinacy region it describes is the starting point for the analysis of optimal policy and of learnability (Bullard and Mitra 2002).

Formalizing it. The result is classical and proved on paper. This mission formalizes the known argument. The mission produces a reusable Lean definition of the basic New Keynesian model, a general lemma on bounded orbits of linear recursions (which applies to any linear rational-expectations model with only forward-looking variables), and a formal Schur–Cohn criterion for real quadratics.

Difficulty

The economic content is elementary, but the obvious argument skips the hardest step. Textbook treatments state "determinacy holds iff both eigenvalues lie outside the unit circle" without proof, and the equivalence between "no nonzero bounded solution" and an eigenvalue condition has to be established for real sequences while the eigenvalues may be complex. In particular the converse direction needs a real bounded solution built from a complex eigenvector, and the boundary case of eigenvalues on the unit circle must come out on the non-determinate side. The parameter translation also has to handle complex-conjugate eigenvalues, not only real ones.

Formalization scope

• Sequences are functions $\mathbb N \to \mathbb R$; the model is the deterministic (shock-free) version, so there are no expectation operators. Stochastic shocks do not change the determinacy condition, but that extension is outside the scope of this mission.
• "Bounded" means a single real bound for all $t$; determinacy requires $y$, $\pi$ and $i$ to be bounded. Boundedness of $i$ follows from that of $y$ and $\pi$, so this adds no restriction.
• Division is Lean's total division; every statement that divides by $\sigma$ or $\beta$ assumes they are nonzero (or positive).
• Eigenvalues are complex roots of the characteristic polynomial of the complexified matrix.
• The goal is not trivial: the zero path is always an equilibrium, determinacy is a genuine uniqueness claim, and the parameter hypotheses are satisfiable (e.g. $\sigma = 1$, $\beta = 0.99$, $\kappa = 0.1$, $\phi_\pi = 1.5$, $\phi_y = 0.5$).
• All declarations live in the namespace DSGE. Contributions of general linear-recursion and polynomial-root lemmas are welcome.

Selected references

• Wikipedia, Dynamic stochastic general equilibrium. https://en.wikipedia.org/wiki/Dynamic_stochastic_general_equilibrium
• O. J. Blanchard and C. M. Kahn, The Solution of Linear Difference Models under Rational Expectations, Econometrica 48(5), 1980. https://doi.org/10.2307/1912186
• F. E. Kydland and E. C. Prescott, Time to Build and Aggregate Fluctuations, Econometrica 50(6), 1982. https://doi.org/10.2307/1913386
• R. Clarida, J. Galí and M. Gertler, The Science of Monetary Policy: A New Keynesian Perspective, Journal of Economic Literature 37(4), 1999. https://doi.org/10.1257/jel.37.4.1661
• J. Bullard and K. Mitra, Learning about Monetary Policy Rules, Journal of Monetary Economics 49(6), 2002. https://doi.org/10.1016/S0304-3932(02)00144-7
• M. Woodford, Interest and Prices: Foundations of a Theory of Monetary Policy, Princeton University Press, 2003.
• J. Galí, Monetary Policy, Inflation, and the Business Cycle, Princeton University Press, 2008 (Chapter 3).

Motivation

In a repeated game, players who do not know the payoff structure can still learn by reinforcement: each player keeps a running score for every action, the cumulative payoff that action would have earned, and plays a mixed strategy that favours actions with high scores. Turning scores into mixed strategies through a regularized best response (maximize score minus a convex penalty) gives a family of dynamics that includes exponential weights and the replicator dynamics (entropic penalty), and also the projection dynamics (quadratic penalty). The same scheme is the continuous-time counterpart of online mirror descent and dual averaging in online optimization.

For the replicator dynamics, the standard folk results of evolutionary game theory say that Nash equilibria are stationary, that limits of interior orbits are Nash equilibria, that Lyapunov stable states are Nash equilibria, and that strict equilibria are asymptotically stable (Weibull 1995; Hofbauer–Sigmund 1998). Mertikopoulos and Sandholm (arXiv:1407.6267v2, Math. Oper. Res. 41(4), 2016) show that all four results survive for the whole family. For steep, decomposable penalties several of them were known (Coucheney–Gaujal–Mertikopoulos 2015). The new part is the nonsteep case, where mixed strategies can hit the boundary of the simplex and the induced dynamics on strategies are no longer well defined.

Setting

A finite game $\mathcal G$ has a finite set $\mathcal N$ of players. Player $k$ has a finite nonempty set $\mathcal A_k$ of pure strategies and a payoff function $u_k:\prod_\ell\mathcal A_\ell\to\mathbb R$. A mixed profile is $x=(x_k)_k\in\mathcal X=\prod_k\Delta(\mathcal A_k)$, and $u_k(x)$ is player $k$'s expected payoff when the players randomize independently. The payoff vector is $v_{k\alpha}(x)=u_k(\alpha;x_{-k})$, the payoff of pure strategy $\alpha$ against $x_{-k}$.

A penalty function on a simplex $\Delta$ (Definition 2.1) is a function $h:\Delta\to\mathbb R$ that is continuous, smooth on the relative interior of every face, and $K$-strongly convex:

$$h(tx_1+(1-t)x_2)\le t\,h(x_1)+(1-t)\,h(x_2)-\tfrac12Kt(1-t)\|x_1-x_2\|_2^2 .$$

Steepness (gradients blowing up at the boundary) is not required. Its choice map is $Q(y)=\arg\max_{x\in\Delta}\{\langle y|x\rangle-h(x)\}$. Every player $k$ has a penalty function $h_k$ with constant $K_k$.

The reinforcement learning dynamics (RL) are

$$\dot y_{k\alpha}=v_{k\alpha}(x),\qquad x_k=Q_k(y_k),$$

and an orbit is a pair $(y(t),x(t))$, $t\ge0$, satisfying them. A Nash equilibrium is a profile $x^*$ with $u_k(x^*)\ge u_k(x_k;x^*_{-k})$ for every $k$ and every mixed $x_k$. It is strict if the inequality is strict for every $x_k\neq x^*_k$.

Because (RL) lives in the space of scores and $Q$ is neither injective nor surjective, stability is defined on the trajectories of play (Definition 5.1):

• $x^*$ is Lyapunov stable if for every $\varepsilon>0$ there is $\delta>0$ such that every orbit with $\|x(0)-x^*\|<\delta$ stays within $\varepsilon$ of $x^*$ forever;
• it is attracting if every orbit started close enough to $x^*$ converges to $x^*$;
• it is asymptotically stable if it is both;
• it is stationary if $x^*\in\operatorname{im}Q$ and every orbit with $x(0)=x^*$ stays at $x^*$.

Formalization targets

Goal: Theorem 5.2, Part IV

$$x^*\ \text{strict Nash equilibrium of }\mathcal G\ \Longrightarrow\ x^*\ \text{asymptotically stable under (RL)},$$

for every finite game and every choice of penalty functions $h_k$, steep or not.

Milestones (the steps of the proof, pp. 23–24, and the Appendix results it uses)

• A strict equilibrium is a pure profile $x^*=(\alpha^*_1,\dots,\alpha^*_N)$, and $\delta_k=\min_{\mu\neq\alpha^*_k}\{v_{k\alpha^*_k}(x^*)-v_{k\mu}(x^*)\}>0$.
• Proposition A.1(iii): $Q_\alpha(y)\to0$ whenever $y_\alpha-y_\beta\to-\infty$.
• Proposition C.3: the Fenchel coupling $F_h(p,y)=h(p)+h^*(y)-\langle y|p\rangle$ satisfies $F_h(p,y)\ge\tfrac12K\|Q(y)-p\|^2$.
• Proposition C.2(i)–(iii): the Bregman divergence $D_h(p,x)=h(p)-h(x)-h'(x;p-x)$, built from the one-sided derivative, is finite, nonnegative with (C.6), and continuous on $\Delta_p=\{x:\operatorname{supp}x\supseteq\operatorname{supp}p\}$.
• (C.11): $F_h(p,y)=D_h(p,Q(y))$ whenever $Q(y)\in\Delta_p$.
• The monotonicity step: $h^*(y)-y_{\alpha^*}=\max_{x}\{\sum_{\mu\ne\alpha^*}x_\mu z_\mu-h(x)\}$ is nondecreasing in the relative scores $z_\mu=y_\mu-y_{\alpha^*}$.

Companions

Theorem 5.2, Parts I–III (stationary $\iff$ Nash and in $\operatorname{im}Q$; limits of orbits and Lyapunov stable states are Nash), Proposition 5.3, Proposition 3.1 (global existence and uniqueness of orbits) and Proposition A.1(i)–(ii).

Significance

Theorem 5.2 says that, as far as the qualitative long-run behaviour is concerned, the whole class of regularized reinforcement dynamics behaves like the replicator dynamics. Part IV is the positive half: strict equilibria are robust attractors of learning. This is used to justify equilibrium selection by learning, and Proposition 5.4 (not part of this mission) builds the rates of convergence, including convergence in finite time for nonsteep penalties, on top of it.

The result is proved in the paper; none of it is formalized. A Lean development would provide a reusable layer of game-theoretic learning dynamics: penalty functions without steepness, choice maps as regularized argmax, the Fenchel coupling and the one-sided Bregman divergence on the simplex. Two companion missions on the same paper use the same layer, for the extinction of dominated strategies and for time averages in zero-sum games. As far as is known, the stability theory of Section 5 has no machine-checked proof even for the replicator dynamics.

Difficulty

The obvious argument would be a Lyapunov argument for the induced dynamics on $\mathcal X$, as for the replicator equation. For nonsteep penalties these dynamics are not well defined: orbits reach the boundary and $Q$ is not invertible there. The proof works in the dual space instead, where the natural Lyapunov candidate is the Fenchel coupling $F_h(x^*,y)$. The coupling is not differentiable along the orbit in the usual sense, and its sublevel sets in score space must be related to genuine neighbourhoods of $x^*$ in $\mathcal X$. That needs the Bregman divergence with one-sided derivatives at boundary points and its continuity across faces of different dimension (Proposition C.2(iii)). A second obstacle is that the coupling does not strictly decrease when the maximizer sits at the vertex. The page states a strict inequality there, which fails for nonsteep penalties, so the argument has to be run with the weak inequality and a first-exit-time argument.

Formalization scope

• The game uses the published agt_games vocabulary: AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash for (5.1). Players form a Fintype ι, and actions are A k with Fintype and DecidableEq.
• Penalty functions are IsPenalty h K, Definition 2.1 with the Euclidean norm in (2.5) and $C^\infty$ smoothness along curves inside the relative interiors of faces. There is no steepness.
• The choice map is the predicate IsChoice h y x, never a chosen argmax.
• Orbits are IsRLOrbit u h y x, the differential form (3.1) with one-sided derivatives at $t=0$. Statements quantify over orbits and never construct one.
• Neighbourhoods of $x^*$ in $\mathcal X$ are balls of the sup metric on $\prod_k\mathbb R^{\mathcal A_k}$, and Definition 5.1 is stated in $\varepsilon$–$\delta$ form.
• Strict equilibria are not assumed pure; purity is a milestone.
• The one-sided derivative (C.3) is a limit predicate with a real value, so the Bregman divergence's value $+\infty$ is never represented by a junk number.
• Proposition 3.1 adds that every $\mathcal A_k$ is nonempty. This is implicit in "finite game", and without it no orbit exists.
• The monotonicity step is stated with $\le$, not the printed $<$.

Trivializing encodings are excluded. Q is not a chosen maximizer that could be chosen badly. Orbit hypotheses are not vacuous: a verification file exhibits an orbit and a strict equilibrium together with a penalty function. Steepness is not added to the hypotheses. The conclusion is genuine convergence $x(t)\to x^*$ together with Lyapunov stability, not a $\liminf$ or a stability-only statement. Proofs of any milestone are welcome. The conjugate and Bregman layer (Appendix C), the regularized-argmax lemmas (Appendix A) and the well-posedness of (RL) (Proposition 3.1) are reusable beyond this mission.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Math. Oper. Res. 41(4), 2016. Cited as arXiv:1407.6267v2. https://arxiv.org/abs/1407.6267v2
• P. Coucheney, B. Gaujal and P. Mertikopoulos, Penalty-regulated dynamics and robust learning procedures in games, Math. Oper. Res. 40(3), 2015. https://doi.org/10.1287/moor.2014.0687
• J. W. Weibull, Evolutionary Game Theory, MIT Press, 1995. https://mitpress.mit.edu/9780262731218/
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• K. C. Kiwiel, Free-steering relaxation methods for problems with strictly convex costs and linear constraints, Math. Oper. Res. 22(2), 1997. https://doi.org/10.1287/moor.22.2.326

Motivation

Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).

Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.

Setting

A 2-player finite game $\mathcal G$ has players $k = 1, 2$, finite pure strategy sets $\mathcal A_k$, and payoff functions $u_k$ on pure profiles. A mixed strategy $x_k$ is a probability vector on $\mathcal A_k$; $\mathcal X$ is the set of mixed profiles $x = (x_1, x_2)$ and $u_k(x)$ the expected payoff (2.1). The payoff vector of player $k$ is $v_{k\alpha}(x) = u_k(\alpha; x_{-k})$, the payoff of the pure strategy $\alpha$ against the opponent's mixed strategy (2.2). A profile $x^*$ is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if $x^*_{k\alpha} > 0$ for every $k$ and $\alpha$. The game is zero-sum if $u_1 = -u_2$.

On the simplex $\Delta$ of a finite set, a penalty function $h$ (Definition 2.1) is continuous on $\Delta$, smooth on the relative interior of every face, and $K$-strongly convex for some $K > 0$:

$$h(tx_1 + (1-t)x_2) \le t h(x_1) + (1-t) h(x_2) - \tfrac12 K t(1-t)\|x_1 - x_2\|^2 .$$

No steepness is required. The choice map is $Q(y) = \arg\max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (Definition 2.2), the convex conjugate is $h^*(y) = \max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (C.1), and the Fenchel coupling is $F_h(p, y) = h(p) + h^*(y) - \langle y|p\rangle$ (C.10).

Each player $k$ has its own penalty function $h_k$. An orbit of (RL) is a pair of trajectories $(y(t), x(t))$, $t \ge 0$, of score vectors and mixed profiles with

$$\dot y_k(t) = v_k(x(t)), \qquad x_k(t) = Q_k(y_k(t)) .$$

The time average of the orbit is $\bar x(t) = t^{-1}\int_0^t x(s)\,ds$.

Formalization targets

Goal: Proposition 6.2 (p. 26)

If $\mathcal G$ is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),

$$\operatorname{dist}\big(\bar x(t), \mathrm{NE}(\mathcal G)\big) \xrightarrow[t\to\infty]{} 0 .$$

The statement fixes no rate and no particular penalty function: it holds for every choice of $h_1, h_2$.

Milestones

1. Proposition C.1 (p. 33): $Q$ is Lipschitz and $Q = dh^*$.
2. Lemma C.6 (p. 36): along (RL), $\frac{d}{dt}F_{h_k}(p_k, y_k(t)) = \langle v_k(x(t)) | x_k(t) - p_k\rangle$.
3. (6.5) (p. 26): in the goal's setting, $F_h(x^*, y(t)) = \sum_k F_{h_k}(x_k^*, y_k(t))$ is constant.
4. Proposition A.1(iii) (p. 31): $Q_\alpha(y) \to 0$ when $y_\alpha - y_\beta \to -\infty$.
5. Proposition C.5 (pp. 35–36): for interior $p$, bounded $F_h(p, y_j)$ forces bounded score differences.
6. Theorem 6.1 (p. 25): in any 2-player game, bounded score differences imply convergence of $\bar x(t)$ to the Nash set.

Significance

The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.

Difficulty

The first idea, comparing $x(t)$ itself with the equilibrium, fails: $x(t)$ need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores $y(t)$, not of $x(t)$, and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: $h$ is not differentiable at the boundary of $\Delta$, yet $h^*$ must be differentiable everywhere on the score space, with derivative $Q$, for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that $v_k$ is linear in the single opponent's strategy, which is specific to two players.

Formalization scope

• Game. Players are Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is $u_0(s) + u_1(s) = 0$ for every pure profile; interiority is $x^*_{k\alpha} > 0$.
• Penalty functions. IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since $K$ is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own $h_k$.
• Choice map and orbits. $x = Q(y)$ is the predicate IsChoice h y x (maximizer of $\langle y|x\rangle - h(x)$ over $\Delta$), never a chosen argmax. An orbit is IsRLOrbit u h y x: for $t \ge 0$, $x_k(t) = Q_k(y_k(t))$ and $\dot y_{k\alpha}(t) = v_{k\alpha}(x(t))$, a right derivative at $t = 0$. This differential form is equivalent to the integral form (RL) because $x$ is continuous along an orbit.
• Time average and convergence. $\bar x(t)$ is defined coordinatewise with the interval integral; only $t \to \infty$ is used. Convergence to the Nash set is Metric.infDist $\to 0$ in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is $0$ in Lean.
• Ruled out. A chosen argmax for $Q$, orbits that are vacuous, steepness added to the penalty, convergence of a subsequence or a liminf in place of the limit, and a Nash set that may be empty are all excluded by the encoding. A sorry-free check exhibits a game, penalty functions and an orbit satisfying all hypotheses of the goal, and verifies that Matching Pennies has the interior equilibrium $((\tfrac12,\tfrac12),(\tfrac12,\tfrac12))$.
• Not included. Theorem 6.3 (chain transitivity under the best-response dynamics) depends on the theory of perturbed solutions of differential inclusions, which is not available. Proposition 6.4 is omitted (see the mission notes).

Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016. Preprint arXiv:1407.6267v2 (cited version). https://arxiv.org/abs/1407.6267
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• J. Hofbauer, S. Sorin and Y. Viossat, Time average replicator and best-reply dynamics, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0359
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.

For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.

Setting

There are $N$ vertices with states $x_i(t)\in\mathbb R^n$. The coupling configuration matrix $G\in\mathbb R^{N\times N}$ has $G_{ij}\ge0$ for $i\ne j$, where $G_{ij}>0$ records a connection from vertex $j$ to vertex $i$, and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. Given a function $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$, a coupling strength $c$, an inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and pinning 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,$$

where the reference $s$ solves $\dot s=f(s,t)$. The network is globally synchronized when $x_i(t)-s(t)\to0$ for every vertex and every pair of solutions.

The nonlinearity is controlled by Assumption 1: there is a matrix $K$ with $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le(x-y)^{\mathsf T}K\Gamma(x-y)$ for all $x,y$ and $t\ge0$. Throughout §4 the paper also assumes that $K$ and $\Gamma$ commute, that $\Gamma$ is positive definite, and puts $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$.

The vertices split into strongly connected components $V_1,\dots,V_M$. In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes $G$ block lower triangular. For each component $j$ the mission uses three matrices:

• $\widetilde G_j$, the diagonal block of $G-\mathrm{diag}(d)$ on $V_j$;
• $A_j$, the within-component part of $G$ with zero row sums;
• $\widetilde\Pi_j=\mathrm{diag}(\Pi_j)$, where $\Pi_j$ is a positive vector with $\Pi_j^{\mathsf T}A_j=0$.

In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.

Formalization targets

Goal: Theorem 4.5

If, for every component $j$,

$$2\theta\widetilde\Pi_j+c\bigl(\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j\bigr)<0, \tag{4.8}$$

then the controlled network with a directed spanning tree is globally synchronized.

Milestones

1. The θ bound (p. 1402). Commutation and $\Gamma>0$ turn Assumption 1 into $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le\theta(x-y)^{\mathsf T}\Gamma(x-y)$.
2. Lemma 2.13. The strict Schur complement test for a symmetric block matrix.
3. Lemma 4.4. If $\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j<0$ on every diagonal block of a block lower-triangular $\overline G$, then positive block weights $\Delta_j$ exist with $\Delta\widetilde\Pi\overline G+\overline G^{\mathsf T}\widetilde\Pi\Delta<0$.
4. (4.10). Along solutions, $V=\sum_j\Delta_j\widetilde e_j^{\mathsf T}\widetilde\Pi_j\widetilde e_j$ satisfies $\dot V\le e^{\mathsf T}\{[\Delta\widetilde\Pi(c\overline G+\theta I_N)+(c\overline G+\theta I_N)^{\mathsf T}\widetilde\Pi\Delta]\otimes\Gamma\}e$.

Companions

• Corollary 4.7: the same conclusion under $\theta\widetilde\Pi_j+c(\overline A_j-\widetilde\Pi_jC_j-\widetilde\Pi_j\overline D_j)<0$, which separates the outer in-degrees $C_j$ from the pinning gains $\overline D_j$.
• Corollary 4.8 (i): an explicit coupling-strength threshold under Assumption 2.
• Corollary 4.9: partial synchronization of the first components.

Significance

Theorem 4.5 replaces a single $Nn\times Nn$ matrix inequality for the whole network with $M$ inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.

On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:

• a reusable strict Schur complement lemma;
• a block-triangular diagonal-stability lemma;
• a template for Lyapunov estimates on coupled networks in Lean.

Difficulty

The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights $\Delta_j$ have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on $[0,\infty)$, a Kronecker-product definiteness argument with $\Gamma$, and the commutation of $K$ and $\Gamma$ to reach the θ bound.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on $[0,\infty)$ through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions $(s,x)$; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on $\mathbb R^n$. "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and $X<0$ is (-X).PosDef. $\lambda_{\max}$ is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.

The vertices are not permuted into Frobenius form. The hypotheses say instead that:

• every component is nonempty;
• every component is strongly connected inside itself;
• every edge between components points forward in the order;
• every vertex is reachable from a pinned vertex.

The weights $\Pi_j$ are tied to the paper's object by $\Pi_j^{\mathsf T}A_j=0$. The standing assumptions of p. 1402 (Assumption 1, $K\Gamma=\Gamma K$, $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$, $\Gamma>0$) are hypotheses of every goal-level statement. The goal does not assume the weights $\Delta_j$, the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For $n=0$ the $\lambda_{\max}$ hypothesis cannot be met, so that degenerate dimension is excluded.

The pages contain three misprints. (4.10) has "$-c$" in its third line and "$++$" in its last; the last line, with a single $+$, is formalized. Corollary 4.9 ranges "$i=1,\dots,N$" where the component range is meant.

A complete development needs a Gronwall-type decay lemma on $[0,\infty)$, the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.

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(6) (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708