Dynamical Systems

Completed

Convex Optimization Optimization·Captain: mikedeng1

Fast Convergence of Inertial Dynamics and Algorithms with Asymptotic Vanishing Viscosity 2: For Strongly Convex Φ and α > 3, Φ(x(t)) − min Φ, ‖x(t) − x*‖² and ‖ẋ(t)‖² Are O(t^(−2α/3))Research Paper

Motivation

Nesterov's accelerated gradient method minimizes a smooth convex function at the rate $\mathcal O(k^{-2})$ in the number of iterations $k$ , against $\mathcal O(k^{-1})$ for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation

\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\nabla\Phi(x(t))=0\tag{1}

with $\alpha=3$ , a heavy-ball system whose friction coefficient $\alpha/t$ vanishes as $t\to+\infty$ (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.

Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general $\alpha$ . This mission formalizes their result for strongly convex $\Phi$ , where the rate of convergence of (1) depends on $\alpha$ and improves without bound as $\alpha$ grows.

Timeline.

2014–2016: Su, Boyd and Candès prove $\Phi(x(t))-\min\Phi=\mathcal O(t^{-2})$ for convex $\Phi$ and $\alpha\ge3$ , and $\mathcal O(t^{-3})$ for strongly convex $\Phi$ when $\alpha>9/2$ ([44, Theorem 4.2] in the paper).
2015 (this paper): every trajectory converges weakly to a minimizer when $\alpha>3$ ; for strongly convex $\Phi$ and every $\alpha>3$ , the values, the squared distance to the minimizer and the squared velocity are $\mathcal O(t^{-2\alpha/3})$ .

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ , and let $\Phi:\mathcal H\to\mathbb R$ be continuously differentiable with gradient $\nabla\Phi$ . Fix $\alpha>0$ and $t_0>0$ . A solution of (1) is a twice differentiable trajectory $x:[t_0,+\infty[\to\mathcal H$ with velocity $\dot x$ satisfying (1) at every $t\ge t_0$ .

$\Phi$ is strongly convex with constant $\mu>0$ if

\Phi(y)\ge\Phi(x)+\langle\nabla\Phi(x),y-x\rangle+\frac\mu2\|x-y\|^2\qquad\text{for all }x,y\in\mathcal H.

Such a $\Phi$ has exactly one minimizer $x^*$ , and $\min\Phi=\Phi(x^*)$ .

For $\lambda\ge0$ , $p\ge0$ the anchored energy is

\mathcal E^p_\lambda(t)=t^p\Big(t^2\big(\Phi(x(t))-\min\Phi\big)+\tfrac12\|\lambda(x(t)-x^*)+t\dot x(t)\|^2\Big),

a sum of nonnegative terms. The proof of the main theorem fixes

p=\tfrac23(\alpha-3),\qquad\lambda=\tfrac23\alpha,\qquad t_1=\max\Big\{t_0,\sqrt{p\lambda/\mu}\Big\}.

Formalization targets

Goal: Theorem 3.4 (p. 11)

For strongly convex $\Phi$ and $\alpha>3$ , every solution $x$ of (1) converges strongly to the unique minimizer $x^*$ , and

\Phi(x(t))-\min\Phi=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|x(t)-x^*\|^2=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|\dot x(t)\|^2=\mathcal O\big(t^{-\frac23\alpha}\big)\tag{25}

as $t\to+\infty$ . The goal states the asymptotic form; the explicit constants are milestones.

Milestones (explicit forms, valid for $t\ge t_1$ )

The derivative identity (10) for $\mathcal E^p_\lambda$ along solutions of (1), for any $\lambda,p\ge0$ .
Its strongly convex upper bound (first display of the proof of Theorem 3.4).
(26): $\mathcal E^p_\lambda(t)\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{4}t^p\|x(t)-x^*\|^2\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{2\mu}t^p(\Phi(x(t))-\min\Phi)$ .
(27): $\Phi(x(t))-\min\Phi\le2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .
(28): $\|x(t)-x^*\|^2\le\frac2\mu(\Phi(x(t))-\min\Phi)\le\frac4\mu\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .
Last display of the proof: $\|\dot x(t)\|^2\le4\big(1+\sqrt{\alpha/(\alpha-3)}\big)^2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .

Significance

The theorem shows that the rate of (1) on strongly convex functions is not capped at $\mathcal O(t^{-2})$ or $\mathcal O(t^{-3})$ : the exponent $2\alpha/3$ grows linearly in $\alpha$ , and it already exceeds $2$ for every $\alpha>3$ . It extends [44, Theorem 4.2], which needs $\alpha>9/2$ and gives $\mathcal O(t^{-3})$ . The same parametrized energy $\mathcal E^p_\lambda$ is the template for the discrete analyses of Nesterov-type algorithms with parameter $\alpha$ , so its derivative identity (10) is reusable beyond this mission.

The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.

Difficulty

The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at $t_0$ , real powers $t^p$ , and the chain rule for $\Phi\circ x$ in an infinite-dimensional space. The obvious argument, that $\mathcal E^p_\lambda$ is nonincreasing, fails: even with the best choice of $p$ and $\lambda$ the bound on its derivative keeps a term $\frac{\lambda p}{2}t^p\langle x-x^*,\dot x\rangle$ of no fixed sign, and only for $t\ge t_1$ is the quadratic term in $\|x-x^*\|^2$ nonpositive. Passing from the differential inequality to (26) therefore needs integration on $[t_1,t]$ for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.

Formalization scope

$\mathcal H$ is any real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$ . $\Phi$ is ContDiff ℝ 1 and $\nabla\Phi$ is Mathlib's gradient.
A solution is a pair $(x,v)$ with $t_0>0$ , where $x$ has derivative $v(t)$ and $v$ has derivative $-\frac\alpha t v(t)-\nabla\Phi(x(t))$ within $[t_0,+\infty[$ at every $t\ge t_0$ ; $\dot x$ is $v$ .
Strong convexity is the gradient inequality printed on p. 10, with $\mu>0$ ; $\min\Phi$ is written $\Phi(x^*)$ with $x^*$ a minimizer.
$t^p$ is the real power, only evaluated at $t\ge t_0>0$ ; $p$ , $\lambda$ , $t_1$ are named definitions shared by the milestones.
$\mathcal O$ in (25) is Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of $x^*$ are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. $\Phi=\|\cdot\|^2$ with $\mu=2$ , and $x\equiv0$ solves (1)).
Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the journal typesetting.

Useful infrastructure: the derivative of $\Phi\circ x$ via gradient, integration of differential inequalities on $[t_0,+\infty[$ , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168 (2018), 123–175. https://doi.org/10.1007/s10107-016-0992-8
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983), 372–376.

9 thms2 active usersReviewed

Control Theory Graph Theory Linear algebra·Captain: mikedeng1

Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators 2: λ₂(L(P_ij cos φ_ij)) > λ_critical Gives Phase Cohesiveness and Exponential Frequency SynchronizationResearch Paper

Motivation

Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.

The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.

Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function $\|H\theta\|_2^2$ , and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants $D_i$ , phase shifts $\varphi_{ij}$ and non-complete graphs, using a weighted Lyapunov function.

Setting

There are $n\ge2$ oscillators with phases $\theta_i$ , time constants $D_i>0$ , natural frequencies $\omega_i\in\mathbb R$ , coupling weights $P_{ij}\ge0$ and phase shifts $\varphi_{ij}\in[0,\pi/2[$ ( $i\ne j$ ), with $P_{ii}=\varphi_{ii}=0$ . The non-uniform Kuramoto model is

D_i\dot\theta_i=\omega_i-\sum_{j=1}^nP_{ij}\sin(\theta_i-\theta_j+\varphi_{ij}),\qquad i=1,\dots,n. \tag{8}

In this mission $P=P^T$ , and its non-zero entries induce a connected graph.

$H\in\mathbb R^{n(n-1)/2\times n}$ is the incidence matrix of the complete graph: $H\theta=(\theta_2-\theta_1,\dots)$ lists all pairwise differences, and $\|H\theta\|_2^2=\sum_{i<j}(\theta_i-\theta_j)^2$ .
$\Delta(\gamma)$ is the set of configurations contained in an open arc of length $\gamma$ , i.e. $\max_{i,j}|\theta_i-\theta_j|<\gamma$ .
The Laplacian of a symmetric matrix $A$ is $L(a_{ij})=\operatorname{diag}(\sum_ja_{ij})-A$ and $\lambda_2(L(a_{ij}))$ is its second-smallest eigenvalue, the algebraic connectivity. The lossless coupling is the matrix $(P_{ij}\cos\varphi_{ij})$ .
$\kappa=\sum_kD_k$ , $\alpha=\sqrt{\min_{i\ne j}\{D_iD_j\}/\max_{i\ne j}\{D_iD_j\}}$ , $\varphi_{\max}=\max_{i,j}\varphi_{ij}$ , $\Omega=\sum_i\omega_i/\sum_iD_i$ .
The critical value is

\lambda_{\mathrm{critical}}=\frac{\|HD^{-1}\omega\|_2+\sqrt n\,\big\|\big[\sum_j\tfrac{P_{1j}}{D_1}\sin\varphi_{1j},\dots,\sum_j\tfrac{P_{nj}}{D_n}\sin\varphi_{nj}\big]\big\|_2}{\cos(\varphi_{\max})(\kappa/n)\alpha/\max_{i\ne j}\{D_iD_j\}}. \tag{33}

The radii $\gamma_{\max}\in\,]\pi/2-\varphi_{\max},\pi]$ and $\gamma_{\min}\in[0,\pi/2-\varphi_{\max}[$ solve $\operatorname{sinc}(\gamma_{\max})/\operatorname{sinc}(\pi/2-\varphi_{\max})=\sin(\gamma_{\min})/\cos(\varphi_{\max})=\lambda_{\mathrm{critical}}/\lambda_2(L(P_{ij}\cos\varphi_{ij}))$ .

Formalization targets

Goal: Theorem V.5 (Synchronization condition II)

If $\lambda_2(L(P_{ij}\cos\varphi_{ij}))>\lambda_{\mathrm{critical}}$ , then

for every $\gamma\in[\gamma_{\min},\alpha\gamma_{\max}]$ the set $\{\theta\in\Delta(\pi):\|H\theta\|_2\le\gamma\}$ is positively invariant, and every solution with $\theta(0)\in\Delta(\pi)$ , $\|H\theta(0)\|_2<\alpha\gamma_{\max}$ eventually satisfies $\|H\theta(t)\|_2\le\gamma$ for every $\gamma>\gamma_{\min}$ ;
for every such solution the frequencies converge exponentially to a common $\dot\theta_\infty\in[\dot\theta_{\min}(0),\dot\theta_{\max}(0)]$ ; if $\varphi\equiv0$ , then $\dot\theta_\infty=\Omega$ and the rate is no worse than

\lambda_{\mathrm{fe}}(\gamma)=\lambda_2(L(P_{ij}))\cos(\gamma)\cos(\angle(D\mathbf 1,\mathbf 1))^2/D_{\max}\qquad(\gamma\in\,]\gamma_{\min},\pi/2[).

Milestones

Lemma V.8 (the identity (36) that replaces $HD^{-1}H^T$ by $\kappa$ ), Lemma V.9 (a quadratic-form bound by $\lambda_2$ ), the sinc estimate and the bound $\tilde X$ on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on $W$ , the existence and uniqueness of $\gamma_{\min},\gamma_{\max}$ from the analysis of (41), and the eventual entry of every trajectory into $\{\|H\theta\|_2<\pi/2-\varphi_{\max}\}$ .

Significance

The condition is checkable from network data: $\lambda_2$ of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to $K>\|H\omega\|_2$ (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.

The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm $\|H\theta\|_2$ is written on p. 23 with a double sum that counts each pair twice; the chain defining $\tilde X$ on p. 25 is printed with its inequalities reversed; and "reaches $\{\|H\theta\|_2\le\gamma_{\min}\}$ " holds only asymptotically. The formal statements make each of these precise.

Difficulty

The obvious Lyapunov function, $\|H\theta\|_2^2$ , has a sign-indefinite derivative as soon as the $D_i$ differ, because the coupling $P_{ij}/D_i$ is not symmetric. The weighted function $W(H\theta)=\frac14\sum_{i,j}D_iD_j|\theta_i-\theta_j|^2$ restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below $\pi$ , the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of $W$ , which are ellipsoids rather than balls of $\|H\theta\|_2$ unless all $D_i$ coincide. The constants $\alpha$ , $\gamma_{\min}$ , $\gamma_{\max}$ come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.

Formalization scope

Configurations are real lifts $\theta\in\mathbb R^n$ ; $\Delta(\pi)$ means $\theta_i-\theta_j<\pi$ for all $i,j$ , and $\|H\theta\|_2$ is the pair-sum norm. A solution is a function $\theta:\mathbb R\to\mathbb R^n$ with right derivative at $0$ and derivative at every $t>0$ equal to the vector field of (8), and statements quantify over every solution. $\dot\theta$ is the vector field evaluated along the solution.
Added hypotheses: $n\ge2$ (needed for $\lambda_2$ and the extrema over $i\ne j$ ), and $\varphi_{ij}=\varphi_{ji}$ , which the page uses silently (the lossless coupling must be a symmetric Laplacian) and which holds for power networks. $P_{ij}\ge0$ off the diagonal, since §V.B allows zero weights.
Corrections: $\|H\theta\|_2$ sums over pairs $i<j$ ; the $\tilde X$ chain is stated as $\|HX\|_2\le\tilde X$ ; the attraction clause of 1) is stated as "eventually below every $\gamma>\gamma_{\min}$ "; the rate of (19) is taken positive (it is printed with a minus sign), and the "Moreover" rate is stated for every $\gamma\in\,]\gamma_{\min},\pi/2[$ because (19) depends on an arc length the theorem does not name. The page's "Moreover, if $\gamma_{\max}=0$ " is read as $\varphi_{\max}=0$ , a misprint: $\gamma_{\max}>\pi/2-\varphi_{\max}$ is never zero.
$\gamma_{\min},\gamma_{\max}$ are quantified subject to their defining equations, and a milestone proves they exist and are unique, so they are not free parameters. Condition (33) is satisfiable (equal ratios $\omega_i/D_i$ and $\varphi\equiv0$ give $\lambda_{\mathrm{critical}}=0$ ), so the goal is not vacuous.
Source: the arXiv preprint v4 of the SICON article; every page and number refers to that preprint.
Infrastructure: weighted graph Laplacians, their second eigenvalue and Courant–Fischer-type bounds, incidence matrices, and ultimate-boundedness arguments for ODEs. The Laplacian and incidence-matrix layer is reusable for consensus and network-dynamics missions; contributions on any milestone are welcome.

Selected references

F. Dörfler, F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; preprint arXiv:0910.5673v4. https://arxiv.org/abs/0910.5673v4
N. Chopra, M. W. Spong, On exponential synchronization of Kuramoto oscillators, IEEE Trans. Automatic Control 54(2), pp. 353–357, 2009 (reference [32] of the source).
A. Jadbabaie, N. Motee, M. Barahona, On the stability of the Kuramoto model of coupled nonlinear oscillators, American Control Conference, Boston, 2004, pp. 4296–4301 (reference [33] of the source).
H. K. Khalil, Nonlinear Systems, 3rd ed., Prentice Hall, 2002 (ultimate boundedness, Theorem 4.18; reference [51] of the source).

14 thms2 active usersReviewed

Control Theory Graph Theory·Captain: mikedeng1

Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators 1: Γ_min > Γ_critical Gives Phase Cohesiveness and Exponential Frequency SynchronizationResearch Paper

Motivation

Transient stability asks whether a power grid, after a large disturbance such as a fault or a line trip, returns to synchronous operation in which all generators rotate at a common frequency. The classical approach builds energy functions for the swing equations and estimates regions of attraction numerically; it gives no closed-form test relating synchronization to the network's parameters, and it handles transfer conductances (losses) only when they are "sufficiently small" without saying how small.

Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) observe that, for strongly overdamped generators, the network-reduced swing equations behave like a first-order non-uniform Kuramoto model, and they give purely algebraic conditions under which this model synchronizes. The same model is a generalization of the classical Kuramoto model of coupled oscillators, studied in physics, neuroscience and control, with heterogeneous time constants, asymmetric effective coupling and phase shifts. This mission formalizes the first of the paper's two synchronization conditions, Theorem V.3, which is also statements 1)–2) of the paper's main result, Theorem III.2.

Setting

There are $n \ge 2$ oscillators with phases $\theta_1, \dots, \theta_n$ . Each has a time constant $D_i > 0$ and a natural frequency $\omega_i \in \mathbb R$ ; each pair has a coupling weight $P_{ij} \ge 0$ and a phase shift $\varphi_{ij} \in [0, \pi/2[$ , with $P_{ii} = \varphi_{ii} = 0$ . The non-uniform Kuramoto model is

D_i\,\dot\theta_i = \omega_i - \sum_{j=1}^n P_{ij}\sin(\theta_i - \theta_j + \varphi_{ij}), \qquad i = 1, \dots, n. \tag{8}

The phases live on the torus. For an arc length $\gamma \in [0, \pi]$ , the set $\Delta(\gamma)$ consists of configurations whose phases all lie in the interior of some arc of length $\gamma$ , and $\bar\Delta(\gamma)$ is its closure (with the synchronized configurations). A set is positively invariant if every solution starting in it stays in it. A solution achieves exponential frequency synchronization if all frequencies $\dot\theta_i(t)$ converge exponentially fast to a common value $\dot\theta_\infty$ .

The condition of the theorem compares two numbers built from the parameters, with $\varphi_{\max} = \max_{i,j}\varphi_{ij}$ :

\Gamma_{\min} := n\min_{i\neq j}\Big\{\frac{P_{ij}}{D_i}\cos\varphi_{ij}\Big\},\qquad \Gamma_{\mathrm{critical}} := \frac{1}{\cos\varphi_{\max}}\Big(\max_{i\neq j}\Big|\frac{\omega_i}{D_i}-\frac{\omega_j}{D_j}\Big| + 2\max_i\sum_{j=1}^n\frac{P_{ij}}{D_i}\sin\varphi_{ij}\Big).

$\Gamma_{\min}$ is the weakest lossless coupling of an oscillator to the network; $\Gamma_{\mathrm{critical}}$ measures the spread of natural frequencies and the losses. When $\Gamma_{\min} > \Gamma_{\mathrm{critical}}$ , put $c = \cos(\varphi_{\max})\Gamma_{\mathrm{critical}}/\Gamma_{\min}$ , $\gamma_{\min} = \arcsin c \in [0, \pi/2-\varphi_{\max}[$ and $\gamma_{\max} = \pi - \arcsin c \in\, ]\pi/2, \pi]$ .

Formalization targets

Goal: Theorem V.3 (Synchronization condition I), corrected

If $P = P^T$ is complete ( $P_{ij} > 0$ for $i \ne j$ ) and

\Gamma_{\min} > \Gamma_{\mathrm{critical}}, \tag{26}

then (1) $\bar\Delta(\gamma)$ is positively invariant for every $\gamma \in [\gamma_{\min}, \gamma_{\max}]$ , and every solution starting in $\Delta(\gamma_{\max})$ eventually stays in $\bar\Delta(\gamma)$ for each $\gamma \in\, ]\gamma_{\min}, \gamma_{\max}]$ ; (2) every solution starting in $\Delta(\gamma_{\max})$ achieves exponential frequency synchronization to some $\dot\theta_\infty$ , and $\dot\theta_\infty \in [\dot\theta_{\min}(0), \dot\theta_{\max}(0)]$ when the solution starts in $\Delta(\pi/2 - \varphi_{\max})$ .

Milestones

The milestones follow the paper's proof. Theorem V.1 is a frequency-synchronization theorem for phase-cohesive oscillators under a globally reachable node, with the explicit rate

\lambda_{fe} = \lambda_2(L(P_{ij}))\cos(\gamma)\cos(\angle(D\mathbf 1, \mathbf 1))^2/D_{\max}

when $\varphi \equiv 0$ and $P = P^T$ . Its supporting steps are the frequency dynamics (20) and a dihedral-angle bound. The phase-cohesiveness argument of Theorem V.3 is split into a trigonometric lower bound, a pointwise bound on the growth rate of the arc containing all phases, the characterization of $[\gamma_{\min}, \gamma_{\max}]$ by inequality (30), positive invariance, and the entry into $\bar\Delta(\pi/2 - \varphi_{\max})$ .

Significance

The theorem turns synchronization of a heterogeneous, lossy oscillator network into one inequality among explicit parameters. For the classical Kuramoto model it specializes to $K > \omega_{\max} - \omega_{\min}$ (Remark V.4), which improved the sufficient conditions known at the time. For power networks it gives, through Theorem III.2, a computable sufficient condition for transient stability when generator inertia is small relative to damping.

To our knowledge none of these results has a machine-checked proof. The development needs ODE comparison arguments for a non-smooth Lyapunov function (the arc length) and an exponential convergence theorem for time-varying consensus. Both are general tools that are not in Mathlib and would be reusable for other consensus and synchronization results. The mission also records two clauses of the printed theorem that are false as stated, with counterexamples, and states the corrected theorem.

Difficulty

The arc length $V(\theta) = \max_{i,j}(\theta_i - \theta_j)$ is only Lipschitz, so its decrease along solutions must be argued through Dini derivatives and a comparison lemma rather than by differentiation. Positive invariance at the boundary $\gamma = \gamma_{\min}$ holds with a non-strict inequality, so a naive "strictly decreasing at the boundary" argument does not apply there. Frequency synchronization rests on a contraction property of linear consensus with time-varying, state-dependent weights. The weights are positive only after the phases have entered $\bar\Delta(\pi/2 - \varphi_{\max})$ . Before that the frequency range can expand, which is why the range clause of the printed theorem fails for initial arcs longer than $\pi/2 - \varphi_{\max}$ .

Formalization scope

Phases are represented by real lifts $\theta : \mathrm{Fin}\,n \to \mathbb R$ . $\bar\Delta(\gamma)$ means that all pairwise differences of the lift are at most $\gamma$ , and $\Delta(\gamma)$ that they are strictly less than $\gamma$ . Conclusions are stated for the same continuous lift, which is at least as strong as membership on the torus. A solution is a map $\theta : \mathbb R \to \mathbb R^n$ with derivative (one-sided at $0$ ) equal to the right-hand side of (8) for all $t \ge 0$ . Every statement quantifies over all such solutions. $\dot\theta$ always denotes the vector field along the solution. Minima and maxima over $i \ne j$ are over ordered pairs, and $n \ge 2$ is assumed so that they exist. The conventions $P_{ii} = \varphi_{ii} = 0$ are explicit hypotheses. $\gamma_{\min}$ and $\gamma_{\max}$ are defined by $\arcsin$ , and a milestone certifies that they are the unique solutions in the printed ranges. $\lambda_2$ is the second-smallest eigenvalue of the symmetric Laplacian.

The source is the arXiv preprint v4 of the SICON article, cited with its own page and theorem numbers. Three corrections relative to the printed text are made and disclosed in the items:

"each trajectory starting in $\Delta(\gamma_{\max})$ reaches $\bar\Delta(\gamma_{\min})$ " holds only asymptotically ( $n = 2$ , $\varphi \equiv 0$ , $D \equiv 1$ , $P_{12} = 1$ , $\omega = (1, 0)$ : the phase difference tends to the equilibrium $\pi/6 = \gamma_{\min}$ without reaching it). It is stated for every $\gamma > \gamma_{\min}$ .
the frequency range $[\dot\theta_{\min}(0), \dot\theta_{\max}(0)]$ fails for some initial conditions in $\Delta(\gamma_{\max})$ ( $n = 2$ , $D \equiv 1$ , $\omega \equiv 0$ , $P_{12} = 1$ , $\varphi_{12} = \varphi_{21} = 1/2$ , $\theta(0) = (2.4, 0)$ ). It is stated for initial conditions in $\Delta(\pi/2 - \varphi_{\max})$ , while exponential synchronization is stated for all of $\Delta(\gamma_{\max})$ .
the rate (19) is printed with a leading minus sign but is used as a positive decay rate. The positive rate is stated.

No statement is trivially satisfiable. The solution predicate holds for actual solutions (for example the synchronous solution), condition (26) is satisfiable (take $\omega \equiv 0$ and $\varphi \equiv 0$ ), the exponential rate is required to be strictly positive, and $\gamma_{\min}, \gamma_{\max}$ are specific numbers rather than existential witnesses.

Contributions are welcome on all milestones. The trigonometric bound, the dihedral-angle bound and the $\gamma_{\min}/\gamma_{\max}$ characterization are elementary. The comparison lemma for Dini derivatives and the consensus contraction theorem are reusable infrastructure.

Selected references

F. Dörfler, F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; preprint arXiv:0910.5673v4. https://arxiv.org/abs/0910.5673v4 — DOI: https://doi.org/10.1137/110851584
L. Moreau, Stability of continuous-time distributed consensus algorithms, 43rd IEEE CDC, 2004 (the contraction theorem cited as [53, Theorem 1]). https://arxiv.org/abs/math/0409010
Y. Kuramoto, Self-entrainment of a population of coupled non-linear oscillators, Int. Symp. on Mathematical Problems in Theoretical Physics, Lecture Notes in Physics 39, 1975. https://doi.org/10.1007/BFb0013365
H.-D. Chiang, F. F. Wu, P. P. Varaiya, Foundations of direct methods for power system transient stability analysis, IEEE Trans. Circuits Syst. 34(2), 1987. https://doi.org/10.1109/TCS.1987.1086115

12 thms2 active usersReviewed

Completed

Pure Mathematics·Captain: wurtle

Ergodicity of triangular billiards with an irrational angleResearch Paper

Motivation

A billiard in a polygon is a point moving at unit speed inside the table and reflecting off the sides by the law "angle of incidence equals angle of reflection". It is one of the simplest Hamiltonian systems and a standard model in mathematical physics; triangles also model two point masses colliding on a segment. The natural invariant probability measure is normalized area times uniform direction, and the basic question is ergodicity: are the only flow-invariant sets of measure $0$ or $1$ ? For polygons with angles that are rational multiples of $\pi$ the answer is no (the phase space splits into invariant surfaces, one for each family of directions). For triangles with an irrational angle the question has been open for every individual triangle, with only generic or specially approximable examples known.

Timeline

1975. Zemlyakov and Katok construct the phase space, show that vertex-hitting trajectories form a null set, and prove topological transitivity for irrational polygons (doi:10.1007/BF01818045).
1986. Kerckhoff, Masur and Smillie prove unique ergodicity in almost every direction for rational polygons, and ergodicity of the full flow for a dense $G_\delta$ set of polygons (doi:10.2307/1971280).
1997. Vorobets gives an explicit approximation condition implying ergodicity, with examples including irrational right triangles (doi:10.1070/SM1997v188n03ABEH000211).
2002. Masur and Tabachnikov survey rational billiards and flat structures (doi:10.1016/S1874-575X(02)80015-7).
2014 and 2022. Numerical studies of irrational right triangles and irrational isosceles triangles raise doubts about ergodicity (doi:10.1103/PhysRevE.89.042918, doi:10.1103/PhysRevE.105.L012201).
2025. Forni and Moll develop a cohomological-equation framework for flat surfaces with cone points, proving constancy of sufficiently regular invariant functions under non-rational holonomy (arXiv:2510.18128).
2026. Chaika and Forni prove weak mixing for a dense $G_\delta$ set of $n$ -gons (doi:10.4007/annals.2026.203.3.1).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims ergodicity for every triangle with at least one irrational angle.

Setting

Let $Q$ be the open interior of a nondegenerate triangle in $\mathbb R^2$ with angles $\alpha,\beta,\gamma$ . The phase space is $Q\times S^1$ (position and unit direction). The billiard flow $\Phi_t$ moves a state in a straight line at unit speed; on reaching an open side it reflects the direction across that side (tangential component preserved, normal component reversed). Trajectories that hit a vertex, in either time direction, have no continuation and are discarded; they form a null set. The invariant probability measure is

d\mu=\frac{dA\,d\theta}{2\pi\,\mathrm{Area}(Q)}.

$\Phi_t$ is ergodic if every measurable $A$ with $\mu(\Phi_t^{-1}A\,\triangle\,A)=0$ for all $t\in\mathbb R$ has $\mu(A)\in\{0,1\}$ .

Formalization targets

Goal: Theorem 1

If at least one of $\alpha/\pi$ , $\beta/\pi$ , $\gamma/\pi$ is irrational, then the billiard flow on $Q\times S^1$ is ergodic for $\mu$ :

\mu(\Phi_t^{-1}A\,\triangle\,A)=0\ \ \forall t\in\mathbb R\quad\Longrightarrow\quad\mu(A)\in\{0,1\}.

The Lean statement OAI.TriangularBilliards.irrational_triangle_billiard also asks for the standard well-posedness facts (almost every state has a unique complete trajectory avoiding vertices, each $\Phi_t$ preserves $\mu$ , and $\Phi_{s+t}=\Phi_s\circ\Phi_t$ almost everywhere), so that the ergodicity clause is about the actual billiard flow. It is open on the platform.

Significance

The theorem settles ergodicity for the entire class of triangles with an irrational angle, including triangles with one rational and two irrational angles, with no genericity or Diophantine condition; earlier results gave ergodicity only for a residual set or for tables with exceptionally fast rational approximations. It also contradicts the non-ergodicity suggested by numerical experiments, which can now be attributed to slow convergence. The paper derives interior and boundary quantum ergodicity of Dirichlet and Neumann eigenbases and growth of nodal-domain counts for these triangles. The claim is ergodicity only, not mixing or unique ergodicity.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.

Difficulty

Triangle sides are straight, so there is no dispersing curvature to drive hyperbolicity, and trajectories near vertices have no continuous continuation. Rational-approximation arguments (Kerckhoff–Masur–Smillie, Vorobets) only reach generic or specially approximable tables. The Forni–Moll framework shows that invariant functions with horizontal Sobolev regularity are constant under non-rational holonomy, but a bounded invariant indicator has no such regularity a priori: one obtains an $L^2$ gradient for each angular Fourier coefficient separately, not a square-summable family, and must show each of these gradients vanishes.

Formalization scope

A Triangle is three affinely independent points of ℂ; table is the interior of their convex hull; side i is an open segment; angle i is the interior angle at vertex i via InnerProductGeometry.angle.
Phase space is ℂ × Circle with the product of normalized area on the table and the uniform angular probability (pushforward of normalized Lebesgue measure on $[0,2\pi)$ ).
A FlightChain is a bi-infinite strictly increasing sequence of collision times, unbounded in both directions, with collisions in open sides, straight flights through the open table, and specular reflection reflect across the side tangent. billiardFlow follows the unique chain if one exists and is the identity otherwise; the theorem must prove the singular set is null.
Ergodicity is stated for measurable sets with $\mu(\Phi_t^{-1}A\triangle A)=0$ for every real $t$ .

A complete development needs the geometry of unfolding, the null measure of vertex-hitting trajectories, Liouville measure preservation for billiards, angular Fourier decomposition on the doubled triangle, and holonomy arguments. Formalizing the well-posedness clauses alone (measure preservation and the a.e. flow property) is reusable for all polygonal billiards and is a welcome first contribution.

Selected references

OpenAI, Ergodicity of triangular billiards with an irrational angle, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026.pdf
A. N. Zemlyakov, A. B. Katok, Topological transitivity of billiards in polygons, Math. Notes, 1975. https://doi.org/10.1007/BF01818045
S. Kerckhoff, H. Masur, J. Smillie, Ergodicity of billiard flows and quadratic differentials, Ann. of Math., 1986. https://doi.org/10.2307/1971280
Ya. B. Vorobets, Ergodicity of billiards in polygons, Sb. Math., 1997. https://doi.org/10.1070/SM1997v188n03ABEH000211
H. Masur, S. Tabachnikov, Rational billiards and flat structures, Handbook of Dynamical Systems, 2002. https://doi.org/10.1016/S1874-575X(02)80015-7
J. Chaika, G. Forni, Weakly mixing polygonal billiards, Ann. of Math., 2026. https://doi.org/10.4007/annals.2026.203.3.1
G. Forni, N. Moll, Cohomological equation for geodesic flows on flat surfaces, preprint, 2025. https://arxiv.org/abs/2510.18128

2 thms2 active usersReviewed

Completed

Analysis·Captain: wurtle

Boundedness and persistence of weakly reversible mass-action systemsResearch Paper

Motivation: can a weakly reversible reaction network lose a species or blow up?

Chemical reaction network theory studies the polynomial differential equations that describe concentrations of interacting species under mass-action kinetics, where each reaction proceeds at a rate proportional to the product of the concentrations of its reactants. A central theme is which properties of the dynamics are forced by the structure of the reaction graph alone, independently of the (usually unknown) rate constants. Weak reversibility — every reaction can be undone by some directed path of reactions — is the main structural condition in this theory. Two long-standing conjectures ask whether weak reversibility alone guarantees that no species dies out (persistence) and that no concentration grows without bound (boundedness). These questions matter for systems biology and chemical engineering, where extinction of a species or unbounded growth would contradict the modeled behavior, and they are closely tied to the global attractor conjecture for complex-balanced systems.

Timeline

1972 — Horn and Jackson develop the equilibrium and stability theory of complex-balanced mass-action systems (ARMA 1972); Horn (ARMA 1972) and Feinberg (ARMA 1972) give complex-balancing criteria and the deficiency-zero analysis.
1987 — Feinberg formulates the expectation that a positive trajectory of a weakly reversible system cannot converge to a boundary point (Chem. Eng. Sci. 1987, Remark 6.1.E).
2010 — August and Barahona state the general boundedness and persistence conclusion (IFAC 2010); the source identifies a gap in one step of their proof (p. 2).
2011 — Anderson separates the boundedness conjecture from the persistence conjecture and proves boundedness for a single linkage class (J. Math. Chem. 2011); he also proves the global attractor conjecture in the single-linkage case (SIAM J. Appl. Math. 2011).
2012–2013 — Pantea proves persistence of bounded trajectories when the stoichiometric subspace has dimension two (SIAM J. Math. Anal. 2012); Craciun, Nazarov and Pantea prove boundedness, persistence and permanence for two-species systems (SIAM J. Appl. Math. 2013).
2014 — Gopalkrishnan, Miller and Shiu prove permanence for strongly endotactic systems (SIAM J. Appl. Dyn. Syst. 2014).
2019–2020 — Boros proves every positive stoichiometric class of a weakly reversible system contains a positive equilibrium (SIAM J. Math. Anal. 2019); Boros and Hofbauer reprove single-linkage permanence (SIAM J. Appl. Dyn. Syst. 2020).
2026 — Craciun's revised toric-differential-inclusion approach gives persistence for bounded trajectories (arXiv:1501.02860v3).
2026 — The OpenAI preprint Boundedness and persistence of weakly reversible mass-action systems (OpenAI Math Release, September 25, 2026) claims both conjectures for constant positive rates in every dimension. It has not been peer reviewed and its theorem is not formally verified.

Setting

Fix $d\ge1$ species. A reaction network consists of a finite set of complexes $\mathcal C\subset\mathbb Z_{\ge0}^d$ and a set $\mathcal R$ of reactions $y\to y'$ with $y,y'\in\mathcal C$ , $y\neq y'$ . It is weakly reversible if for every reaction $y\to y'$ there is a directed path of reactions from $y'$ back to $y$ . Given positive rate constants $\kappa_{y\to y'}>0$ , the mass-action system is

\dot x = f(x)=\sum_{y\to y'\in\mathcal R}\kappa_{y\to y'}\,x^{y}\,(y'-y),\qquad x^y=\prod_{i=1}^d x_i^{y_i}.

A positive trajectory is persistent if $\liminf_{t\to\infty}x_i(t)>0$ for every $i$ .

In Lean (namespace OAI.Problem326), a ReactionNetwork d has a Finset of complexes in Fin d → ℕ and a Finset of reactions between them with distinct source and target; WeaklyReversible is Relation.TransGen reachability from target back to source; massAction N κ is the vector field above; and IsGlobalForwardSolution N κ x0 x means $x(0)=x_0$ and $x$ has derivative $f(x(t))$ at every $t\ge0$ .

Formalization targets

Goal: global existence, boundedness and persistence (Theorem 1.1)

Let $d\ge1$ , let the network be weakly reversible and all rates positive. For every $x^0\in\mathbb R_{>0}^d$ the solution with $x(0)=x^0$ exists for all $t\ge0$ , and there is $\varepsilon\in(0,1)$ , depending on the network, the rates and $x^0$ , such that

\varepsilon\le x_i(t)\le\varepsilon^{-1}\qquad(t\ge0,\ 1\le i\le d).

The goal is published on the platform with status Open.

Significance

The result itself. The theorem proves the boundedness conjecture and the persistence conjecture together, for arbitrary constant positive rates, any number of linkage classes and any number of species; earlier results needed a single linkage class, two species, or a two-dimensional stoichiometric subspace. It applies whether or not the stoichiometric compatibility class is bounded. Combined with complex balance, it yields convergence to the unique positive equilibrium in each class (the global attractor conclusion; Remark 3.5, p. 15). The proof also produces, for each positive initial point, a compact convex forward-invariant polytope in the open orthant (Proposition 3.3, p. 13), which gives a short proof of Boros's existence theorem for positive equilibria (Corollary 3.4, p. 14).

Formalizing it. Statements about reaction networks quantify over all networks and all rates, so they are a natural fit for formal verification; the history includes a published proof with a gap in one step. A machine-checked proof would settle the status of the general theorem independently of that history.

Difficulty

The natural approach is to find a Lyapunov function or an invariant region whose boundary each reaction crosses inward. Individual reactions need not point inward across any fixed face, and near the orthant boundary and at infinity different monomials dominate in different regions, with ties between monomials that an arbitrary choice of face normal can reverse. The argument must control the combined flux across cuts of the reaction graph using the return paths given by weak reversibility, and must do so simultaneously for small and large concentrations; a naive comparison of monomials by total degree fails, as the source's example $2A\rightleftarrows B$ with $(a,b)=(T,T^3)$ shows.

Formalization scope

Complexes are vectors in Fin d → ℕ, so exponents are nonnegative integers and $f$ is a polynomial vector field on $\mathbb R^d$ ; the reaction set is a Finset with source ≠ target. Empty reaction sets and isolated complexes are allowed, as in the source.
Rates are a function on reactions with ∀ e, 0 < κ e; $d>0$ is a hypothesis.
The conclusion asserts existence of some global forward solution and bounds for every global forward solution from $x^0$ (uniqueness is therefore not assumed). Solutions are functions ℝ → (Fin d → ℝ) with HasDerivAt at every $t\ge0$ , including a two-sided derivative at $t=0$ .
The same $\varepsilon$ works for all $t\ge0$ and all species; it may depend on $x^0$ . No uniformity over initial points is claimed.
Needed infrastructure: Picard–Lindelöf for polynomial fields, forward invariance of convex polytopes (Nagumo-type tangency conditions), and graph-cut flux estimates. ODE invariance tools are reusable beyond this mission.

Selected references

F. Horn and R. Jackson, General mass action kinetics, Arch. Rational Mech. Anal. 47 (1972). https://doi.org/10.1007/BF00251225
M. Feinberg, Complex balancing in general kinetic systems, Arch. Rational Mech. Anal. 49 (1972). https://doi.org/10.1007/BF00255665
M. Feinberg, Chemical reaction network structure and the stability of complex isothermal reactors — I, Chem. Eng. Sci. 42 (1987). https://doi.org/10.1016/0009-2509(87)80099-4
E. August and M. Barahona, Solutions of weakly reversible chemical reaction networks are bounded and persistent, IFAC Proc. Vol. 43 (2010). https://doi.org/10.3182/20100707-3-BE-2012.0018
D. F. Anderson, Boundedness of trajectories for weakly reversible, single linkage class reaction systems, J. Math. Chem. 49 (2011). https://doi.org/10.1007/s10910-011-9886-4
C. Pantea, On the persistence and global stability of mass-action systems, SIAM J. Math. Anal. 44 (2012). https://doi.org/10.1137/110840509
G. Craciun, F. Nazarov and C. Pantea, Persistence and permanence of mass-action and power-law dynamical systems, SIAM J. Appl. Math. 73 (2013). https://doi.org/10.1137/100812355
M. Gopalkrishnan, E. Miller and A. Shiu, A geometric approach to the global attractor conjecture, SIAM J. Appl. Dyn. Syst. 13 (2014). https://doi.org/10.1137/130928170
B. Boros, Existence of positive steady states for weakly reversible mass-action systems, SIAM J. Math. Anal. 51 (2019). https://doi.org/10.1137/17M115534X
G. Craciun, Toric differential inclusions and a proof of the global attractor conjecture, arXiv:1501.02860v3, 2026. https://arxiv.org/abs/1501.02860v3
OpenAI, Boundedness and persistence of weakly reversible mass-action systems, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026/paper.pdf

2 thms2 active usersReviewed

Algorithmic Game Theory Linear algebra·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 1: Near the Two-Player Unit-Disk Game Γ₀ of Section II, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

Learning in games asks whether players who adjust their strategies over time, by simple rules, end up at a Nash equilibrium. Many adaptive dynamics share one informational feature: each player's adjustment depends on the current play and on that player's own payoff function, but not on the payoffs of the others. Hart and Mas-Colell (AER 2003) call such dynamics uncoupled, and show that this feature alone rules out guaranteed convergence to Nash equilibrium, even for families of games in which every game has exactly one equilibrium. Earlier non-convergence results, such as Shapley's example for fictitious play and the cycling examples of Jordan (1993) and Foster and Young (1998), concern particular dynamics; this one applies to the whole class of uncoupled dynamics. It is one reason the learning literature turned to weaker targets such as correlated equilibrium, which regret-based uncoupled procedures do reach (Hart and Mas-Colell, Econometrica 2000).

The paper proves its theorem in two settings: a two-player game with a continuum of strategies (§II and the Appendix) and a three-player game with two strategies each (§III). This mission formalizes the first setting.

Setting

There are two players, $i=1,2$ , and $j=3-i$ denotes the other player. Each player's strategy set is the closed unit disk $D=\{z\in\mathbb R^2:\|z\|\le1\}$ , and a profile is $x=(x^1,x^2)\in X:=D\times D$ . A game $\Gamma=(u^1,u^2)$ is a pair of payoff functions on $X$ . A profile $\bar x$ is a (pure) Nash equilibrium if no player gains by changing only their own strategy. A dynamic for a family $\mathcal U$ of games is a vector field $F(x;\Gamma)$ on $X$ for each $\Gamma\in\mathcal U$ , read $\dot x=F(x;\Gamma)$ . It is uncoupled if $F^i$ depends on the game only through $u^i$ : two games of $\mathcal U$ in which player $i$ has the same payoff function give the same $F^i(x;\cdot)$ at every $x\in X$ .

A dynamic is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ with its Nash equilibrium $\bar x(\Gamma)$ :

$F(\cdot\,;\Gamma)$ is $C^1$ on $X$ ;
$F(\bar x(\Gamma);\Gamma)=0$ ;
all eigenvalues of the $4\times4$ Jacobian matrix of $F(\cdot\,;\Gamma)$ at $\bar x(\Gamma)$ have negative real parts;
every solution $x(t)$ converges to $\bar x(\Gamma)$ as $t\to\infty$ , from any initial condition.

The game $\Gamma_0$ has payoffs $u_0^i(x^i,x^j)=-\|x^i-\varphi(x^j)\|^2$ . Here $\varphi:D\to D$ is continuous, $\varphi(z)=2z$ for $\|z\|\le\frac13$ , $\varphi$ rotates the unit circle by $\pi/4$ , and $\varphi$ is affine on rays in between. The family $\mathcal U_0$ consists of the games $u^i(x^i,x^j)=-\|x^i-\xi^i(x^j)\|^2$ with continuous $\xi^i:D\to D$ such that $\xi^i(\xi^j(x^i))=x^i$ has a unique solution. Every such game has a unique Nash equilibrium, and $\Gamma_0\in\mathcal U_0$ has the equilibrium $(0,0)$ .

Formalization targets

Goal: THEOREM 1 for the game $\Gamma_0$ of §II

Let $\mathcal U$ be a family in which each game has a single Nash equilibrium and which contains every game of $\mathcal U_0$ within some $\eta>0$ of $\Gamma_0$ . Then

F\ \text{uncoupled for}\ \mathcal U\ \Longrightarrow\ F\ \text{is not Nash-convergent for}\ \mathcal U.

Milestones

the explicit $\varphi$ has the two required properties, and rotates by an angle in $[0,\pi/4]$ (fn. 21);
every game of $\mathcal U_0$ has a unique Nash equilibrium, and that of $\Gamma_0$ is $(0,0)$ ;
Lemma 2: for an uncoupled Nash-convergent dynamic on $\mathcal U_0$ , at a unique best reply $F^i=0$ and the own-strategy Jacobian block $J^i$ has eigenvalues with negative real parts;
the derivative identity, giving the Jacobian at $\Gamma_0$ the block form

J=\begin{bmatrix}J^1&-2J^1\\-2J^2&J^2\end{bmatrix};

the coefficient $a_3=3\det(J^1)\operatorname{tr}(J^2)+3\det(J^2)\operatorname{tr}(J^1)$ of $\lambda$ in $\det(J-\lambda I)$ , and Lemma 3: if $J^1,J^2$ are stable, then $J$ has an eigenvalue with positive real part;
the main-text result: no uncoupled dynamic is Nash-convergent for $\mathcal U_0$ ;
the Appendix: the functions $\psi_a$ satisfy conditions (1)–(4), and the conclusions of Lemma 2 at $\Gamma_0$ already follow from the games of $\mathcal U_0$ near $\Gamma_0$ .

A companion statement, that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent, shows that the notion of Nash-convergence can be met.

Significance

The theorem identifies an informational obstruction rather than a computational one. Convergence to Nash equilibrium is easy if the dynamic may use the whole game, as the coupled dynamic $\dot x=\bar x(\Gamma)-x$ shows. It fails once each player may react only to their own payoff function, and the failure persists on an arbitrarily small neighborhood of a single game. It explains why no natural adaptive procedure has been found that converges to Nash equilibrium in general, and it motivates the stochastic, finite-memory and correlated-equilibrium variants studied afterwards (for example Hart and Mas-Colell, GEB 2006).

The result is proved in the paper. As far as the curators know, it has no machine-checked proof. A formalization fixes the model precisely. That matters here, because the conclusion depends on details the prose treats lightly: which perturbations the family must contain, what the Jacobian is at boundary points, and which solutions count.

Difficulty

The obvious argument fails because an uncoupled dynamic is a different vector field for each game, and nothing forces the fields to fit together except the uncoupledness constraint. The proof extracts information about $F(\cdot\,;\Gamma_0)$ from auxiliary games that share one player's payoff with $\Gamma_0$ , and in which that player's best reply is constant. Making those auxiliary games lie in the family is the delicate part: in $\mathcal U_0$ they are immediate, but near $\Gamma_0$ they require the functions $\psi_a$ of the Appendix, whose fixed-point conditions (3) and (4) rest on an angle argument. The linear-algebra step is exact: the stability of $J^1$ and $J^2$ must be shown to force instability of the coupled $4\times4$ matrix through the sign of one coefficient of its characteristic polynomial.

Formalization scope

$\mathbb R^2$ is modelled as $\mathbb C$ , and rotation by $\theta$ is multiplication by $e^{i\theta}$ . Players are Fin 2, 0-based, and the other player is i + 1. A game is a pair of real functions on $\mathbb C^2$ , but every definition looks only at its values on $X=D\times D$ . Nash equilibria are pure equilibria in $X$ (fn. 9 notes there are no mixed ones). Derivatives are Fréchet derivatives within $X$ . Eigenvalue conditions use the published predicate FatkhullinPolyak.Discrete.IsHurwitz, with the $4\times4$ Jacobian indexed in player-major order. The $C^1$ and Jacobian conditions, which the paper imposes on every dynamic it considers, are part of NashConvergent. The single-Nash-equilibrium property is a hypothesis of the goal.

Two encodings are deliberate:

The neighborhood. " $\mathcal U$ contains a neighborhood of $\Gamma_0$ " is read as the Appendix reads it: $\mathcal U$ contains every game of $\mathcal U_0$ close to $\Gamma_0$ in the sense of fn. 7. This is implied by the literal hypothesis, so the formal theorem is at least as strong. A full neighborhood contains games with several equilibria, so together with the single-equilibrium hypothesis it would make the theorem vacuous.
Solutions. Solutions are curves that stay in $X$ . If curves were allowed to leave $X$ , they would follow values of $F$ that no game constrains, and Nash-convergence would fail for every $F$ , which makes the goal trivial. The goal must also not be met through an empty family: the hypotheses are jointly satisfiable, for instance by $\{\Gamma\in\mathcal U_0:\Gamma\text{ within }1\text{ of }\Gamma_0\}$ .

The development needs:

calculus of $C^1$ maps on a product of disks;
spectra of real matrices viewed over $\mathbb C$ and the characteristic polynomial of a $4\times4$ block matrix;
elementary planar geometry of rotations and radial interpolation.

The linear-algebra milestones (block Jacobian, $a_3$ , Lemma 3) are independent of game theory and reusable. Contributions are welcome on any milestone, in any order.

Selected references

S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5), 1830–1836, 2003. https://doi.org/10.1257/000282803322655581
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5), 1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153
J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3), 368–386, 1993. https://doi.org/10.1006/game.1993.1022
D. P. Foster and H. P. Young, On the Nonconvergence of Fictitious Play in Coordination Games, Games and Economic Behavior 25(1), 79–96, 1998. https://doi.org/10.1006/game.1997.0615
S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2), 286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear algebra·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 2: Near Jordan's Three-Player Game Γ₀ of Section III, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

A central question of the theory of learning in games is whether simple adaptive behavior leads players to a Nash equilibrium. Many natural dynamics — fictitious play, best-reply dynamics, replicator dynamics — fail to converge in some games, and the failures are usually exhibited one dynamic at a time. Hart and Mas-Colell (AER 2003) asked a structural question instead: is there any continuous-time dynamic, satisfying one informational restriction, that converges to Nash equilibrium for all games in a reasonable family? The restriction is uncoupledness: each player's adjustment may depend on the current strategy profile and on that player's own payoff function, but not on the payoff functions of the others. This is the situation of players who do not know the opponents' preferences.

Their answer is negative, and the paper proves it with two examples. This mission formalizes the second, built on a three-player game introduced by James Jordan (GEB 1993) in his study of learning mixed-strategy equilibria. A companion mission formalizes the first example, a two-player game on the unit disk.

Setting

Three players each choose between two pure strategies, $0$ and $1$ . A game $\Gamma$ is identified with its payoff functions $(u^1,u^2,u^3)$ , $u^i:\{0,1\}^3\to\mathbb R$ . A state is a mixed profile $x=(x^1,x^2,x^3)\in X=[0,1]^3$ , where $x^i$ is the probability that player $i$ plays $0$ (top row, left column, left matrix). Payoffs extend to $X$ by expectation over independent randomizations, and $\bar x$ is a Nash equilibrium when no player can raise its expected payoff by changing its own coordinate.

Jordan's family $\mathcal U_0$ consists of the games

u^i(s)=\begin{cases}a^i & s^i=0,\ s^{i+1}=1,\\ 1 & s^i=1,\ s^{i+1}=0,\\ 0&\text{otherwise,}\end{cases}

indices modulo 3, with parameters $a^i$ close to $1$ : each player wants to mismatch the next player. Jordan's game $\Gamma_0$ is the member with all $a^i=1$ ; every game of $\mathcal U_0$ has a unique Nash equilibrium $\bar x^i(\Gamma)=a^{i-1}/(a^{i-1}+1)$ , and $\bar x(\Gamma_0)=(1/2,1/2,1/2)$ .

A dynamic for a family $\mathcal U$ is a vector field $\dot x=F(x;\Gamma)$ on $X$ , one for each $\Gamma\in\mathcal U$ . It is uncoupled if $F^i(x;\Gamma)=F^i(x;\Gamma')$ whenever $\Gamma,\Gamma'\in\mathcal U$ give player $i$ the same payoff function. When every game of $\mathcal U$ has a single Nash equilibrium $\bar x(\Gamma)$ , $F$ is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ , $\bar x(\Gamma)$ is a rest point, every solution converges to it, $F(\cdot;\Gamma)$ is $C^1$ , and the Jacobian $J$ of $F(\cdot;\Gamma)$ at $\bar x(\Gamma)$ is hyperbolic and stable: all its eigenvalues have negative real parts.

Formalization targets

Goal: Theorem 1 near Jordan's game

Let $\mathcal U$ have the single-Nash-equilibrium property and contain every game of $\mathcal U_0$ that is close to $\Gamma_0$ . Then

\text{no uncoupled dynamic for }\mathcal U\text{ is Nash-convergent for }\mathcal U .

Milestones

Every game of $\mathcal U_0$ (indeed every $a$ with all $a^i>0$ ) has the unique equilibrium $\bar x^i=a^{i-1}/(a^{i-1}+1)$ ; in particular $\bar x_0=(1/2,1/2,1/2)$ .
If $F$ is uncoupled and Nash-convergent, then $f=F(\cdot;\Gamma_0)$ satisfies $f^i(\bar x_0+(y-\tfrac12)e_i)=0$ for $y$ near $1/2$ , hence the diagonal and the trace of $J=Df(\bar x_0)$ vanish:

\operatorname{tr}J=0.

A real $3\times3$ matrix with zero trace and nonzero determinant has an eigenvalue with positive real part.

Two further items record the paper's observations: uncoupledness forces $J=\begin{pmatrix}0&c&0\\0&0&d\\e&0&0\end{pmatrix}$ , and such a matrix has an eigenvalue with positive real part when $cde\ne0$ and spectrum $\{0\}$ otherwise. A last item shows that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent.

Significance

The theorem says that convergence to Nash equilibrium is not a property that adaptive dynamics can deliver on informational grounds alone: as soon as a family contains the games near $\Gamma_0$ , any rule in which players respond only to their own payoffs fails for some game, even though every game in the family has a unique equilibrium and a coupled rule converges for all of them. The finite example matters because it shows that the obstruction is not an artifact of continuum strategy spaces: it occurs in a $2\times2\times2$ game in mixed strategies. The paper contrasts it (§IV) with the existence of uncoupled dynamics that converge to correlated equilibria: Nash equilibrium cannot be reached in an uncoupled way, while correlated equilibrium, a notion based on coordination, can. Follow-up work extends the impossibility to stochastic uncoupled dynamics (Hart and Mas-Colell, GEB 2006) and surveys the area (Hart, Econometrica 2005).

The result has been proved since 2003; no machine-checked proof of it is known. A formal proof requires an equilibrium computation in a parametric family of finite games, a careful treatment of the derivative of a vector field defined only on a cube, and a spectral fact about real $3\times3$ matrices. The definitions of uncoupled and Nash-convergent dynamics written here are reusable for other impossibility results of the same kind.

Difficulty

The obvious attempt is to analyze a particular dynamic and show that it cycles around $\bar x_0$ . That proves nothing about other dynamics: the statement quantifies over every uncoupled $F$ , so the argument must extract a constraint on $F$ from uncoupledness alone. Uncoupledness only relates the dynamic at different games through single coordinates of $F$ , and Nash-convergence only constrains $F$ at the equilibria of the games in $\mathcal U$ ; neither says anything directly about the Jacobian at $\Gamma_0$ . Formally, the delicate steps are the uniqueness of the equilibrium for all nearby parameters, which requires excluding pure and partially mixed equilibria, and the passage from vanishing along a segment to a vanishing partial derivative.

Formalization scope

Players are indexed $0,1,2$ in Lean (the page's player $i$ is index $i-1$ ), strategies are Fin 2, and a game is Fin 3 → (Fin 3 → Fin 2) → ℝ. The state space is $X=[0,1]^3\subset\mathbb R^3$ ; a dynamic is any map $F:\mathbb R^3\times\text{Game}\to\mathbb R^3$ , whose values outside $X$ never matter. Committed conventions:

Solutions stay in $X$ : a solution is a curve on $[0,\infty)$ with values in $X$ satisfying the ODE (one-sided derivative at $0$ ). Allowing curves that leave $X$ would let the junk values of $F$ outside $X$ falsify convergence for every $F$ and trivialize the goal.
Uncoupledness is required only between games of $\mathcal U$ and only at states of $X$ .
Nash-convergence bundles four clauses for every game of $\mathcal U$ and every Nash equilibrium of it: rest point, $C^1$ on $X$ , all eigenvalues of the Jacobian with negative real part (the published FatkhullinPolyak.Discrete.IsHurwitz), and convergence of every solution. The Jacobian is the derivative within $X$ .
The single-Nash-equilibrium property of $\mathcal U$ is a hypothesis of the goal.
The neighborhood hypothesis. The page assumes that $\mathcal U$ contains a neighborhood of $\Gamma_0$ . The goal assumes less: $\mathcal U$ contains every game of $\mathcal U_0$ in some footnote-7 neighborhood of $\Gamma_0$ . The page's hypothesis implies this one, so the formal goal is at least as strong. The literal hypothesis is not used because it is not known (and not claimed on the page) to be compatible with the single-equilibrium property, and a contradictory pair of hypotheses would make the goal vacuous.
Milestone 1 assumes only $a^i>0$ instead of $|a^i-1|<\varepsilon$ for small $\varepsilon$ ; this covers every such family with $\varepsilon\le1$ .

The family $\mathcal U$ cannot be vacuous: Jordan's games with $|a^i-1|<1/2$ satisfy both hypotheses, and the coupled-dynamic item certifies that Nash-convergence itself can be met, so the goal's force rests on uncoupledness. Contributions welcome include the equilibrium computation for $\mathcal U_0$ , the spectral lemmas (which are independent of game theory), and the calculus step from vanishing along a segment to a vanishing partial derivative within a cube.

Selected references

S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5):1830–1836, 2003. https://doi.org/10.1257/000282803322655581
J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3):368–386, 1993. https://doi.org/10.1006/game.1993.1022
S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2):286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007
S. Hart, Adaptive Heuristics, Econometrica 73(5):1401–1430, 2005. https://doi.org/10.1111/j.1468-0262.2005.00625.x

6 thms2 active usersReviewed

Operations Research Stochastic Systems Theoretical Computer Science·Captain: mikedeng1

The Power of Two Choices in Randomized Load Balancing I: In the Limiting Supermarket System the Expected Time Converges to T_d(λ) = Σ λ^((d^i−d)/(d−1))Research Paper

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$ . With two choices it is exponentially smaller as $\lambda \to 1^-$ . This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$ , proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$ , $0<\lambda<1$ , at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$ . Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$ .

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$ , $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$ . The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$ . As $n \to \infty$ the tails follow the limiting system

\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}

A trajectory is a map $t \mapsto s(t)$ , $t \ge 0$ , whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$ ). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$ , so $\pi_0 = 1$ , $\pi_1 = \lambda$ , $\pi_2 = \lambda^{1+d}$ . A customer arriving in state $s$ becomes the $i$ -th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).

The target constant is

T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$ , $T_d(\lambda) < \infty$ , and:

\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$ .
Theorem 2. If $s_j(0) = 0$ for some $j$ , there are constants $N \ge 1$ , $0<\alpha<1$ , $\beta>1$ , $\gamma>0$ , independent of $t$ , with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$ , $t \ge 0$ . From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$ .
Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ( $\delta > 0$ ) whenever $\Phi(0) < \infty$ , and in particular whenever $s_j(0) = 0$ for some $j$ .
Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$ , or $s_j(0) = 0$ for some $j$ ), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$ .
Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$ .
Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$ .

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$ , an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$ , including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$ -bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$ , while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$ , $0 < \lambda < 1$ in every theorem.
A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$ , with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$ : right derivative at $t = 0$ , two-sided for $t > 0$ .
Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$ , and $T_d$ 's $i$ -th term is $\lambda^{\sum_{1\le k<i} d^k}$ .
$\Phi$ , the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$ , so a divergent series is $\infty$ , never a default $0$ . "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$ ; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
Time is real and $t \to \infty$ is Filter.atTop.
Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$ ), dropping the summability condition in Lemma 2 ( $(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333

8 thms2 active usersReviewed

Completed

Control Theory Operations Research·Captain: mikedeng1

Dynamic Instabilities and Stabilization Methods in Distributed Real-Time Scheduling of Manufacturing Systems 4: A Run-Truncating Priority-Queue Supervisor Keeps Every Buffer Bounded When ρₘ < 1Research Paper

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$ , with level $x_{p,i}(t)\ge 0$ . Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$ , and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$ . Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$ , the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}

and thresholds $z_{p,i}\ge0$ . It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$ ; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$ ; when a run ends and $Q_m\ne\emptyset$ , the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$ , the backlog of part type $p$ for machine $\mu_{p,i}$ .

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$ , every supervised trajectory, from every initial state, satisfies

\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$ , that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$ .
A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$ ) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$ .
Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$ .

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$ ; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$ , with a set-up paid at each.

Formalization scope

Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$ . Time is real with $t\ge0$ . Set-up times satisfy $\delta_{b,b}=0$ : a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$ , and at exactly $1/\tau_b$ while $b$ is nonempty.
Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$ . The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$ , are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$ .
Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$ . Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$ : with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$ , never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$ .
Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$ . A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085

8 thms2 active usersReviewed

Operations Research Probability Random Matrix Theory·Captain: mikedeng1

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$ . For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$ . His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$ . Kingman's conditions (§1.1–1.2) are:

S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ ;
S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$ ;
S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$ ;
S₃′: $E(x_{01}^+)<\infty$ , where $x^+=\max(x,0)$ .

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$ .

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$ . A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$ -valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,

with $\log 0=-\infty$ . Expectations of $[-\infty,\infty)$ -valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$ , defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$ .

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$ , then

\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|

exists in $-\infty\le\xi<\infty$ with probability one, and

E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

(1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$ .
Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$ .
Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$ .
Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$ , then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$ . For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$ , as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$ -algebra on $\mathfrak B\times\mathfrak B$ , so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$ . The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$ -algebra, not equality of one-dimensional marginals.
S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
$\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$ ; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$ , and is ruled out.
$\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$ , and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

8 thms2 active usersReviewed

Operations Research Probability Random Matrix Theory·Captain: mikedeng1

Subadditive Ergodic Theory 4: Furstenberg–Kesten — for Stationary Positive Random Matrices, n⁻¹ log [Y₁⋯Y_n]_ij Converges, Independently of i and jResearch Paper

Products of random matrices

Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product $X_n = Y_1 Y_2 \cdots Y_n$ of random matrices and its growth as $n\to\infty$ .

The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, $n^{-1}\log$ of the size of $X_n$ converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.

Timeline:

1960: Furstenberg and Kesten prove convergence of $n^{-1}\log\|X_n\|$ and, for positive matrices, of $n^{-1}\log[X_n]_{ij}$ .
1968: Kingman proves the subadditive ergodic theorem (J. Roy. Statist. Soc. B 30).
1973: Kingman's survey deduces the positive-matrix theorem (Theorem 5) and the general Banach-algebra version (Theorem 6) from it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $k\ge1$ , and let $Y_1, Y_2,\dots$ be random $k\times k$ real matrices. Write $[A]_{ij}$ for the $(i,j)$ th entry of a matrix $A$ , and

X_n = Y_1 Y_2\cdots Y_n \qquad (2.2.1),

the product taken left to right. The sequence $(Y_n)$ is stationary if the joint law of $(Y_2, Y_3, \dots)$ equals the joint law of $(Y_1, Y_2, \dots)$ ; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.

The proof works with the diagonal process

z_{st} = [Y_{s+1}Y_{s+2}\cdots Y_t]_{11},\qquad x_{st} = -\log z_{st}\qquad (s<t),

and with the $\ell_1$ -norm $\|A\| = \max_i \sum_j |[A]_{ij}|$ . A family $(x_{st})_{s<t}$ is a subadditive process (§1.1) if S₁: $x_{su}\le x_{st}+x_{tu}$ for $s<t<u$ ; S₂: the joint distributions of $(x_{s+1,t+1})$ equal those of $(x_{st})$ ; S₃: $g_t=E(x_{0t})$ exists and $g_t\ge -At$ for some constant $A$ .

Formalization targets

Goal: Theorem 5

Suppose the elements of the matrices $Y_n$ are strictly positive, $E|\log[Y_n]_{ij}|<\infty$ for every $n$ and every $i,j$ , and $(Y_n)$ is stationary. Then there is one finite random variable $\lambda$ such that for every $(i,j)$

\lambda = \lim_{n\to\infty} n^{-1}\log [X_n]_{ij} \qquad (2.2.2)

with probability one and in mean. The limit is random in general (it is constant when $(Y_n)$ is ergodic); the theorem asserts its existence, its finiteness and its independence of $(i,j)$ , and nothing about its value.

Milestones, in the order of the paper's proof

(2.3.1): $[AB]_{11}\ge[A]_{11}[B]_{11}$ for matrices with strictly positive entries.
$x_{st}=-\log z_{st}$ satisfies S₁ and S₂, and each $x_{st}$ has finite expectation $g_{t-s}$ .
$E\{\log\|Y_1\|\}<\infty$ and $g_n/n\ge -E\{\log\|Y_1\|\}$ for all $n\ge1$ , so S₃ holds.
The limit (2.2.2) exists, with probability one and in mean, for $i=j=1$ .
(2.2.3): for every $(i,j)$ , $P\{\liminf n^{-1}\log[X_n]_{ij}\ge\lambda\}=1$ .
For every $(i,j)$ , $P\{\limsup n^{-1}\log[X_n]_{ij}\le\lambda\}=1$ .

Significance

The limit $\lambda$ is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of $X_n$ . It governs the stability of random linear recursions $v_{n}=v_{n-1}Y_n$ , the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.

The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.

Difficulty

Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because $\log[X_n]_{11}$ is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling $n^{-1}\log[Y_n]_{1j}$ along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about $X_n'=Y_2\cdots Y_{n+1}$ back to $X_n$ by stationarity, where the limit $\lambda$ is itself random. The natural shortcut — treating $\lambda$ as a constant — is only valid under ergodicity, which is not assumed.

Formalization scope

Matrices are Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index $1$ is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for $n\ge1$ ; Y 0 plays no role.
Products are ordered: $Y_{s+1}\cdots Y_t$ is the List.prod of [Y (s+1), …, Y t]; $X_0$ is the identity.
Stationarity is equality of the laws of $(Y_{n+2})_{n\ge0}$ and $(Y_{n+1})_{n\ge0}$ on ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.
Positivity holds for every outcome; "their logarithms have finite expectations" is integrability of every $\log[Y_n]_{ij}$ , $n\ge1$ .
"Finite limit" is a real-valued lam : Ω → ℝ; "in mean" is $E|n^{-1}\log[X_n]_{ij}-\lambda|\to0$ with $\lambda$ integrable; time is $n\in\mathbb N$ with Filter.atTop. One lam serves all $(i,j)$ .
Lim inf and lim sup inequalities are stated with $\varepsilon$ : almost surely, for every $\varepsilon>0$ , eventually $n^{-1}\log[X_n]_{ij}\ge\lambda-\varepsilon$ (respectively $\le\lambda+\varepsilon$ ), which avoids the junk value of a real liminf on unbounded sequences.
Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.
The S₁/S₂ vocabulary of §1.1 comes from the group's shared process module; this mission defines $g_t$ locally. The general subadditive ergodic theorem is not restated here, and milestone 4 is the object-specific statement the paper writes.

Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31(2):457–469, 1960. https://doi.org/10.1214/aoms/1177705909
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

9 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Subadditive Ergodic Theory 3: A Separable Continuous-Parameter Subadditive Process with E(Ω_I) < ∞ Has x₀ₜ/t → ξ with Probability One and in Mean, E(ξ) = γResearch Paper

Motivation

Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.

The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.

Setting

Work on a probability space $(S,\mathcal F,P)$ . A continuous-parameter subadditive process is a family of real random variables $x_{st}$ indexed by $0\le s<t$ . It satisfies $x_{su}\le x_{st}+x_{tu}$ whenever $0\le s<t<u$ . Its stationarity says that, for every real shift $\tau\ge0$ , the complete shifted family $(x_{s+\tau,t+\tau})_{s<t}$ has the same joint distribution as $(x_{st})_{s<t}$ . Finally, the mean $g_t=E(x_{0t})$ exists as a finite real number for each $t>0$ and obeys $g_t\ge-At$ for one constant $A$ . These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.

For an interval $I\subseteq[0,\infty)$ , the oscillation is $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$ . A process has the local oscillation condition when $E(\Omega_I)<\infty$ for one nondegenerate interval $I$ . In §1.4 the paper states that this condition then holds on every bounded interval. The quantity $\gamma=\inf_{t>0}g_t/t$ is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).

The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.

Formalization targets

Theorem 4: convergence at all real times

For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable $\xi$ such that

\frac{x_{0t}}{t}\longrightarrow\xi\quad\text{almost surely and in }L^1(P) \quad(t\to\infty,\ t\in\mathbb R), \qquad E(\xi)=\gamma=\inf_{u>0}\frac{g_u}{u}.

The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.

Significance

Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.

The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus $L^1$ limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.

Difficulty

An integer-time subadditive theorem controls $x_{0n}/n$ only on its discrete skeleton. It cannot by itself rule out large values of $x_{0t}/t$ for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in $\Omega_I$ also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.

The paper's displayed assertion (1.4.1), that $g_t/t$ converges as real $t\to\infty$ under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).

Formalization scope

Lean indexes the family by $\mathbb R\to\mathbb R\to S\to\mathbb R$ and uses only $0\le s<t$ ; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of $x_{0t}$ for every $t>0$ and one linear lower bound on its mean. The sample-space type is called $S$ so that $\Omega_I$ denotes oscillation without ambiguity.

Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval $[a,b]$ with $0\le a<b$ ; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and $\xi$ is integrable. No continuity of paths, ergodicity, or independence is assumed.

A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. DOI: 10.1214/aop/1176996798.

7 thms2 active usersReviewed

Completed

Probability Stochastic Systems·Captain: mikedeng1

Subadditive Ergodic Theory 2: For Every Increasing Γ There Is a C^∞ Process with Stationary Increments and P{|y_t| ≤ Γ(t) for All Large t} = 0Research Paper

Motivation

Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process $x=(x_{st})$ the ratio $x_{0t}/t$ converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with $t$ ranging over $[0,\infty)$ .

Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process $(y_t;\,t\ge0)$ with stationary increments and finite expectations has a finite limit $\lim_{t\to\infty}y_t/t$ with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$ .

Setting

A real-time process is a family $(y_t;\,t\ge0)$ of real random variables on a probability space $(\Omega,\mathcal F,P)$ . Its joint law is the law of the path $t\mapsto y_t$ on $\mathbb R^{[0,\infty)}$ with the product $\sigma$ -algebra, that is, the collection of all finite-dimensional distributions.

$(y_t)$ is stationary if for every $\tau\ge0$ the shifted process $(y_{t+\tau})_{t\ge0}$ has the same joint law as $(y_t)_{t\ge0}$ .
$(y_t)$ has stationary increments if for every $\tau\ge0$ the process $(y_{t+\tau}-y_\tau)_{t\ge0}$ has the same joint law as $(y_t-y_0)_{t\ge0}$ .
$(y_t)$ has finite expectations if $E|y_t|<\infty$ for every $t\ge0$ .
The sample function at $\omega\in\Omega$ is $t\mapsto y_t(\omega)$ . It has derivatives of all orders if it is $C^\infty$ on $[0,\infty)$ .

A growth bound is a function $\Gamma:(0,\infty)\to(0,\infty)$ that is increasing (non-decreasing). The event " $|y_t|\le\Gamma(t)$ for all sufficiently large $t$ " is the set of $\omega$ for which some $T$ exists with $|y_t(\omega)|\le\Gamma(t)$ for every real $t\ge T$ .

In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.

Formalization targets

Goal: Theorem 3 (p. 888)

For every positive non-decreasing $\Gamma$ on $(0,\infty)$ there are a probability space and a process $(y_t;\,t\ge0)$ with stationary increments, finite expectations and $C^\infty$ sample functions such that

P\{|y_t|\le\Gamma(t)\ \text{for all sufficiently large }t\}=0. \tag{1.4.4}

The quantifiers are "for every $\Gamma$ there exists $y$ ". Because $\Gamma$ may grow arbitrarily fast, no normalization $y_t/a(t)$ with a deterministic $a$ can converge to a finite limit almost surely.

Milestones

The milestones are the four steps of Kingman's proof, stated for the explicit process $y_t=Y_{t+\eta}$ of (1.4.5) built from a bump function $\psi$ , a uniform $\eta$ and independent integer-valued $\nu_0,\nu_1,\dots$ with a law $m_\Gamma$ that depends on $\Gamma$ :

$(y_t)$ is stationary, hence has stationary increments, and its sample functions are $C^\infty$ (p. 888).
$E(|y_t|)=E(y_0)=\int_0^1\psi(u)\,du<\infty$ (p. 888).
$\sum_{n\ge1}P\{\nu_n>\Gamma(n+\tfrac12)\}\ge\sum_{n\ge1}\sum_{r\ge n}\frac1{r(r+1)}=\infty$ (p. 889).
$P\{|y_t|\le\Gamma(t)\text{ eventually}\}\le P\{|y(n+\tfrac12\nu_n^{-1}-\eta)|\le\Gamma(n+\tfrac12\nu_n^{-1}-\eta)\text{ eventually}\}\le P\{\nu_n\le\Gamma(n+\tfrac12)\text{ eventually}\}=0$ (p. 889).

Significance

The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as $E(\Omega_I)<\infty$ in Theorem 4, or the integrability of $\int_I|y'|$ in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so $y_n/n$ converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.

Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on $[0,\infty)$ are reusable beyond this mission.

Difficulty

The natural first attempt is a process with linear or polynomial growth, such as $y_t=Zt$ with a heavy-tailed integrable $Z$ . Every such attempt fails against a $\Gamma$ that grows faster, so the process must depend on $\Gamma$ . A process that is large on a whole interval of length one cannot have finite mean when $\Gamma$ grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift $\tau$ , not only for integer shifts.

Formalization scope

The process is y : ℝ → Ω → ℝ, with values at $t<0$ ignored; $\Omega$ lives in Type. Every $y_t$ with $t\ge0$ is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.
Joint laws are push-forwards to Set.Ici (0:ℝ) → ℝ with the product $\sigma$ -algebra. Stationary increments compare the laws of $(y_{t+\tau}-y_\tau)_t$ and $(y_t-y_0)_t$ for every real $\tau\ge0$ .
"Increasing" is non-decreasing on $(0,\infty)$ (MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. $\Gamma$ is a total function on $\mathbb R$ ; its values at $t\le0$ are irrelevant.
"Derivatives of all orders" is ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on $[0,\infty)$ for every $\omega$ . This is $C^\infty$ , not the analytic order.
In (1.4.4) "sufficiently large $t$ " ranges over real $t$ . The event need not be measurable a priori; $P$ of a set is its outer measure.
A statement with a fixed $\Gamma$ , with $\exists\Gamma$ , with "for some large $t$ ", or with $t$ restricted to the integers would be trivial or false and is not the theorem. The integer skeleton is precisely what does not fail.
For the milestones, the random ingredients are hypotheses: any $\eta,\nu_0,\nu_1,\dots$ that are independent, with $\eta$ uniform on $(0,1)$ and each $\nu_r$ of law $m_\Gamma$ . The existence of such a family is part of the goal's proof.

Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society, Series B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

7 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Stability and Instability of Fluid Models for Reentrant Lines 3: In Every Reentrant Line the Last-Buffer-First-Served Fluid Model Is StableResearch Paper

Motivation

A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).

The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.

Setting

There are $K$ classes, numbered in route order, and $I$ stations. Every unit of fluid enters class $1$ at rate one. On completing service in class $k$ , it becomes class $k+1$ ; after class $K$ , it leaves. The station serving class $k$ is $\sigma(k)$ . Different classes may share a station. The constituency of station $i$ is $C_i=\{k:\sigma(k)=i\}$ , and class $k$ has positive mean service requirement $m_k$ , so its service rate is $\mu_k=1/m_k$ . The nominal workload at station $i$ is $\rho_i=\sum_{k\in C_i}m_k$ . The paper assumes $\rho_i<1$ at every station. Dai and Weiss (1996), pp. 115–117.

For time $t\ge0$ , $Q_k(t)$ is the amount of fluid in class $k$ , and $T_k(t)$ is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each $Q_k$ remains nonnegative, each $T_k$ starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.

A priority ranking $\pi$ assigns a distinct rank to every class, with smaller rank meaning higher priority. For class $k$ , let $H_k$ contain the classes at the same station whose rank is at least as high as $k$ 's. In a preemptive-resume priority fluid model, capacity unused by $H_k$ may increase only when the fluid workload in $H_k$ is zero. Under LBFS, $\pi(k)=K+1-k$ : a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.

Formalization targets

Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and $\rho_i<1$ :

\exists\delta>0\;\forall (Q,T),\quad \bigl[(Q,T)\text{ is an LBFS fluid solution and }|Q(0)|=1\bigr] \Longrightarrow \forall t\ge\delta,\;Q(t)=0,

where $|Q(0)|=\sum_{k=1}^K Q_k(0)$ . The same $\delta$ must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.

The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time

\delta=\frac{|Q(0)|}{\widehat\lambda-1},\qquad \widehat\lambda=\frac{1}{\max_{1\le i\le I}\rho_i}>1.

The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.

Significance

The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.

Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.

Difficulty

The load inequalities $\rho_i<1$ compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.

Formalization scope

Lean represents classes and stations by finite index types. Their indices start at zero: Lean class $k-1$ corresponds to paper class $k$ , and LBFS is Fin.revPerm. The paths $Q$ and $T$ are functions on all real times, while the fluid equations and conclusions are imposed only for $t\ge0$ . The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.

The service requirements $m_k>0$ are explicit so $\mu_k=1/m_k$ has its intended value. The drift and emptying-time milestones explicitly assume $K>0$ , since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when $K=0$ , its normalization $|Q(0)|=1$ is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.

Selected references

J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

8 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Stability and Instability of Fluid Models for Reentrant Lines 2: In Every Reentrant Line the First-Buffer-First-Served Fluid Model Is StableResearch Paper

Why priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$ , becomes class $k+1$ when class $k$ is completed, and leaves after class $K$ . Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ , and $\mu_k = 1/m_k$ . The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$ , and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$ . The exogenous arrival rate is $1$ . The standing assumption of the paper is

\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$ , the fluid levels, and $T(t) = (T_k(t))_k$ , the cumulative service time given to each class, such that for $t \ge 0$ :

Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t), \qquad Q_k(t) \ge 0,

with $\mu_0T_0(t) = t$ ; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$ . Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$ , $T_k^+ = \sum_{l\in H_k}T_l$ , $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$ . Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$ , so earlier steps of the route have priority.

The fluid model is stable (Definition 1.3) if there is a time $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$ .

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$ .

Formalization scope

Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$ .
Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$ .
Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
$m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$ .
In Lemma 2.2 (ii) the printed strict " $\dot g(t) < -\varepsilon$ " is relaxed to " $\le -\varepsilon$ ", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
In the inductive step, "stay empty for $t > t_{k-1}$ " is read as $t \ge t_{k-1}$ , and the case $Q_k(t_{k-1}) = 0$ is included.
The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$ , so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. https://doi.org/10.1287/moor.21.1.115
J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159

8 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 7: Weak Limit Points of the Occupation Measures of a Weak Asymptotic Pseudotrajectory Are InvariantResearch Paper

Motivation

Stochastic approximation algorithms are recursions $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ driven by small steps $\gamma_n$ and noise $U_{n+1}$ ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.

The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically $\gamma_n=o(1/\log n)$ or $\gamma_n=O(n^{-\alpha})$ . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order $1/\log n$ the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.

Setting

A semiflow on a metric space $(M,d)$ is a continuous map $\Phi:\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ for $t,s\ge0$ . Throughout, $M$ is a separable metric space with its Borel $\sigma$ -algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space and $\{\mathcal F_t\}_{t\ge0}$ a nondecreasing family of sub- $\sigma$ -algebras. A process $X:\mathbb R_+\times\Omega\to M$ is a weak asymptotic pseudotrajectory of $\Phi$ if

it is progressively measurable: for every $T>0$ the restriction of $X$ to $[0,T]\times\Omega$ is measurable for the product of the Borel $\sigma$ -field of $[0,T]$ and $\mathcal F_T$ ;
for each $\alpha>0$ and $T>0$ , almost surely

\lim_{t\to\infty}P\Big\{\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)\ge\alpha\ \Big|\ \mathcal F_t\Big\}=0 .

Let $\mathcal P(M)$ be the space of Borel probability measures on $M$ with the topology of weak convergence. A measure $\mu\in\mathcal P(M)$ is $\Phi$ -invariant if $(\Phi_t)_*\mu=\mu$ for every $t\ge0$ ; the set of invariant measures is $\mathcal M(\Phi)$ . The occupation measure of the process at time $t>0$ is the random probability measure

\mu_t(\omega)=\frac1t\int_0^t\delta_{X(s,\omega)}\,ds ,

and $\mathcal M(X,\omega)\subset\mathcal P(M)$ is the set of its weak limit points as $t\to\infty$ .

Formalization targets

Goal: Theorem 10.1

If $X$ is a weak asymptotic pseudotrajectory of $\Phi$ , there is a set $\tilde\Omega\subset\Omega$ with $P(\tilde\Omega)=1$ such that for all $\omega\in\tilde\Omega$

\mathcal M(X,\omega)\subset\mathcal M(\Phi).

No tightness is assumed, so $\mathcal M(X,\omega)$ may be empty; the statement asserts the inclusion, not nonemptiness.

Milestones

Fix a uniformly continuous $f:M\to[0,1]$ and $T>0$ , and set $U_n(f,T)=\int_{(n-1)T}^{nT}f(X(s))\,ds$ for $n\ge1$ . The milestones are the numbered displays of the proof on pp. 62–63:

Eq. (47): $\frac1n\sum_{i=1}^n[U_i(f,T)-E(U_i(f,T)\mid\mathcal F_{(i-1)T})]\to0$ almost surely (stated for every continuous $f$ with values in $[0,1]$ , since the proof also applies it to $f\circ\Phi_T$ );
Eq. (50): the same with $U_{i+1}(f,T)$ conditioned on $\mathcal F_{(i-1)T}$ ;
Eq. (51): $E(U_{i+1}(f,T)-U_i(f\circ\Phi_T,T)\mid\mathcal F_{(i-1)T})\to0$ almost surely;
Eq. (52): $\frac1n\sum_{i=1}^nU_{i+1}(f,T)-\frac1n\sum_{i=1}^nU_i(f\circ\Phi_T,T)\to0$ almost surely;
Eq. (53): for a single measurable path whose occupation measures converge weakly to $\mu$ along $t_j\to\infty$ , the averages $\frac1{n_jT}\sum_{i=0}^{n_j-1}\int_{iT}^{(i+1)T}f(x_s)\,ds$ with $n_j=\lfloor t_j/T\rfloor$ converge to $\int f\,d\mu$ for every bounded continuous $f$ .

Significance

The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, $\mathcal M(X,\omega)$ is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in $\mathcal M(X,\omega)$ ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.

Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in $\mathcal P(M)$ .

Difficulty

The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space $M$ , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.

Formalization scope

Time is $\mathbb R_{\ge0}$ ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; $\mathcal P(M)$ is ProbabilityMeasure M with its topology of weak convergence. $M$ is a separable metric space with its Borel $\sigma$ -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every $T>0$ . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's $P\{\cdot\mid\mathcal F_t\}$ presupposes an event); the supremum over $h\in[0,T]$ is taken in $[0,\infty]$ . Invariance for the semiflow is $(\Phi_t)_*\mu=\mu$ for all $t\ge0$ , the form the proof establishes; for a flow it agrees with the definition $\mu(A)=\mu(\Phi_t(A))$ of Section 8.3. Weak limit points are cluster points of $t\mapsto\mu_t(\omega)$ as $t\to\infty$ ; the occupation measure is a genuine probability measure for every measurable path and $t>0$ .

The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to $0$ and which would make condition 2 vacuous; invariance defined through images $\Phi_t(A)$ , which need not be Borel for a semiflow; and a compactness or Polish assumption on $M$ , which the theorem does not make.

A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. Section 10, Theorem 10.1, pp. 60–63. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617

10 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 1: Limit Sets of Precompact Asymptotic Pseudotrajectories Are Internally Chain TransitiveResearch Paper

Motivation

A stochastic approximation algorithm updates an estimate by small noisy steps, $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ , with step sizes $\gamma_n\to0$ and noise $U_n$ . Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation $\dot x=F(x)$ . Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.

Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of $F$ , and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).

Timeline. Bowen (1975) and Conley (1978) introduced $(\delta,T)$ -pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.

Setting

Let $(M,d)$ be a metric space. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ . A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$ ; then $\Phi|A$ denotes the restricted semiflow on $A$ .

A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory of $\Phi$ if

\lim_{t\to\infty}\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)=0\quad\text{for every }T>0,

and it is precompact if $X(\mathbb R_+)$ has compact closure. Its limit set is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$ .

For $\delta>0$ , $T>0$ , a $(\delta,T)$ -pseudo-orbit from $a$ to $b$ consists of $k\ge1$ partial trajectories, given by points $y_0,\dots,y_{k-1}$ (and an endpoint $y_k$ ) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$ , $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$ , and $y_k=b$ . One writes $a\hookrightarrow b$ if such pseudo-orbits exist for all $\delta,T>0$ . A nonempty compact invariant set $\Lambda$ is internally chain transitive if $a\hookrightarrow b$ for the restricted semiflow $\Phi|\Lambda$ for all $a,b\in\Lambda$ , so that all $y_i$ lie in $\Lambda$ ; it is internally chain recurrent if $a\hookrightarrow a$ for $\Phi|\Lambda$ for every $a\in\Lambda$ . An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ such that $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly in $x\in W$ .

Formalization targets

Goal: Theorem 5.7 (i)

For every semiflow $\Phi$ on a metric space $M$ and every precompact asymptotic pseudotrajectory $X$ of $\Phi$ ,

L(X)\ \text{is internally chain transitive.}

Milestones (in the order of the proof)

Lemma 3.1. $X$ is an asymptotic pseudotrajectory iff $d(\Theta^t(X),\hat\Phi\circ\Theta^t(X))\to0$ , where $\Theta$ is the translation semiflow on $C^0(\mathbb R_+,M)$ and $\hat\Phi(Y)=\Phi^{Y(0)}$ .
Theorem 3.2. For precompact continuous $X$ : $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of $\Theta^{t}(X)$ , $t\to\infty$ , is a trajectory of $\Phi$ ; and then $\{\Theta^t(X)\}_{t\ge0}$ is relatively compact.
Lemma 5.2. A nonempty open $U$ with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ contains an attractor whose basin contains $\overline U$ .
Proposition 5.3. For nonempty $\Lambda$ : internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact, invariant and $\Phi|\Lambda$ has no proper attractor.
Theorem 5.5. On a nonempty compact $M$ , the chain recurrent set $R(\Phi)$ is internally chain recurrent.
Corollary 5.6. If $\overline{\gamma^+(x)}$ is compact, then $\omega(x)$ is internally chain transitive.

Significance

The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).

Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.

Difficulty

The obvious approach follows $X$ from a point $a\in L(X)$ to a point $b\in L(X)$ : $X$ returns near $a$ and near $b$ infinitely often, and on windows of length $T$ it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve $X$ , not in $L(X)$ ; this only shows that $L(X)$ is chain transitive for $\Phi$ on $M$ , a strictly weaker property. Producing pseudo-orbits whose points lie in $L(X)$ itself is the central difficulty, and it is where precompactness of $X$ is used. Invariance $\Phi_t(L(X))=L(X)$ , with equality, also needs a compactness argument, since a semiflow is not invertible.

Formalization scope

A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; $M$ is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality $\Phi_t(A)=A$ . Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype $\Lambda$ , so every point of the pseudo-orbit lies in $\Lambda$ . Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on $C^0(\mathbb R_+,M)$ (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write $C^0(\mathbb R,M)$ , but with the convention $\Phi^p(t)=p$ for $t<0$ that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of $C^0(\mathbb R_+,M)$ .

Ruled out: pseudo-orbits with no trajectory piece ( $k=0$ ), pseudo-orbits allowed to leave $L(X)$ , invariance as mere inclusion $\Phi_t(A)\subset A$ , and any compactness assumption on $M$ . Each of these makes the goal weaker than the theorem of the notes.

A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between $\Phi$ and the translation semiflow on $S_\Phi$ . Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

12 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 2: Under A1 and A2 the Interpolated Process Is an Asymptotic Pseudotrajectory of the Flow of FResearch Paper

Motivation

A stochastic approximation algorithm is a recursion

x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)

in $\mathbb R^d$ , driven by a vector field $F$ , decreasing step sizes $\gamma_n$ and perturbations $U_n$ . Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation $\dot x=F(x)$ .

Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of $\{x_n\}$ is an asymptotic pseudotrajectory of the flow of $F$ . Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.

Setting

Let $F:\mathbb R^d\to\mathbb R^d$ be continuous. It is globally integrable if through every point there is exactly one integral curve $y:\mathbb R\to\mathbb R^d$ , $\dot y=F(y)$ ; the flow $\Phi_t(p)$ is the value at time $t$ of the integral curve through $p$ .

The step sizes satisfy $\gamma_n\ge0$ , $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ . Set $\tau_0=0$ , $\tau_n=\sum_{i=1}^n\gamma_i$ , and $m(t)=\sup\{k\ge0:\tau_k\le t\}$ . The affine interpolated process $X:\mathbb R_+\to\mathbb R^d$ and the piecewise constant processes $\overline X,\overline U,\bar\gamma$ are, for $0\le s<\gamma_{n+1}$ ,

X(\tau_n+s)=x_n+s\,\frac{x_{n+1}-x_n}{\gamma_{n+1}},\qquad \overline X(\tau_n+s)=x_n,\quad \overline U(\tau_n+s)=U_{n+1},\quad \bar\gamma(\tau_n+s)=\gamma_{n+1}.

The noise enters through

\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\overline U(s)\,ds\Big\| .

A1: for every $T>0$ , $\sup\{\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\|:n<k\le m(\tau_n+T)\}\to0$ as $n\to\infty$ ; equivalently $\Delta(t,T)\to0$ as $t\to\infty$ .
A2: $\sup_n\|x_n\|<\infty$ .
A2′: $F$ is Lipschitz and bounded on a neighbourhood of $\{x_n\}$ .

A continuous $X:\mathbb R_+\to\mathbb R^d$ is an asymptotic pseudotrajectory of $\Phi$ if for every $T>0$

\lim_{t\to\infty}\sup_{0\le h\le T}\big\|X(t+h)-\Phi_h(X(t))\big\|=0 .

Formalization targets

Goal: Proposition 4.1

F\ \text{continuous, globally integrable},\quad \text{A1},\quad \text{A2 or A2}'\quad\Longrightarrow\quad X\ \text{is an asymptotic pseudotrajectory of}\ \Phi .

No rate and no constant appear; the statement holds under either alternative.

Milestones

Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$ .
A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$ .
Theorem 3.2: for a flow on a metric space and a continuous $X$ with relatively compact image, $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of the translates $\Theta^t(X)$ in $C^0(\mathbb R,M)$ is a trajectory of the flow; both imply that $\{\Theta^t(X)\}$ is relatively compact.
Comparison of $X$ and $\overline X$ (p. 13): if $\|F(x_n)\|\le K$ , then for $t$ large, $\sup_{t\le u\le t+T}\|X(u)-\overline X(u)\|\le2\Delta(t-1,T+1)+\sup_{t\le u\le t+T}K\bar\gamma(u)$ .
Estimate (11): under A1 and A2′, for $t$ large,

\sup_{0\le h\le T}\|X(t+h)-\Phi_h(X(t))\|\le C(T)\Big[\Delta(t-1,T+1)+\sup_{t\le s\le t+T}\bar\gamma(s)\Big],

with $C(T)$ depending only on $T$ and on $F$ (through its Lipschitz constant and bound on the neighbourhood).

Significance

Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for $L^q$ -bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of $\dot x=F(x)$ . The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.

The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.

Difficulty

The obvious argument compares $X$ directly with the flow by Gronwall's inequality. It needs $F$ Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where $F$ is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.

Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where $F$ is controlled for the whole window $[t,t+T]$ .

Formalization scope

Space $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; $\gamma_0$ and $U_0$ are unused.
$m(t)$ is the largest $k$ with $\tau_k\le t$ , so the divisor $\gamma_{m(t)+1}$ is positive even when some steps vanish.
Limits are written with $\varepsilon$ ; the suprema that remain ( $\Delta$ , $\sup\bar\gamma$ ) are over bounded nonempty sets, and $\overline U$ is a step function with finitely many pieces on bounded intervals, so no integral or supremum takes a default value.
The flow of $F$ is a function satisfying the integral-curve property, together with global integrability (existence and uniqueness of integral curves on $\mathbb R$ ); continuity of the flow is not assumed.
A2′ is read with a uniform neighbourhood: $F$ is Lipschitz and bounded on $\{y:\operatorname{dist}(y,\{x_n\})<r\}$ for some $r>0$ . Under the reading "some open set containing $\{x_n\}$ " the proposition fails for unbounded iterates.
Theorem 3.2 is stated for flows on $C^0(\mathbb R,M)$ (compact-open topology); for semiflows with the convention $\Phi^p(t)=p$ for $t<0$ , the implication (i)⇒(ii) is false as printed.

Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), $X$ is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.

A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on $C^0(\mathbb R,M)$ , continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of $X$ and $\overline X$ are the natural entry points.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probab. Theory Related Fields 74 (1987), 403–428. https://doi.org/10.1007/BF00699098
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
L. Ljung, Analysis of recursive stochastic algorithms, IEEE Trans. Automat. Control 22 (1977), 551–575. https://doi.org/10.1109/TAC.1977.1101561

9 thms2 active usersReviewed

Geometry & Topology·Captain: Lucas

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

Motivation

Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field $X$ on a closed manifold $M$ is Anosov when the tangent bundle splits as $TM=E^s\oplus\mathbb RX\oplus E^u$ , with $E^s$ uniformly contracted and $E^u$ uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.

The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.

Setting

A plug $(U,X)$ is a compact 3-manifold $U$ with boundary and a nonsingular C¹ vector field $X$ transverse to $\partial U$ . The boundary splits into the entrance boundary $\partial^{in}U$ (where $X$ points inwards) and the exit boundary $\partial^{out}U$ . The maximal invariant set $\Lambda$ consists of the points whose orbit stays in $U$ for all times. The plug is hyperbolic if $\Lambda$ is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination $L^s_X=W^s(\Lambda)\cap\partial^{in}U$ and the exit lamination $L^u_X=W^u(\Lambda)\cap\partial^{out}U$ are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of $\partial^{in}U\setminus L^s_X$ (and of $\partial^{out}U\setminus L^u_X$ ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.

A diffeomorphism $\varphi:\partial^{out}U\to\partial^{in}U$ is a strongly transverse gluing map if $\varphi_*(L^u_X)$ and $L^s_X$ are transverse and cut $\partial^{in}U$ into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold $U/\varphi$ with an induced vector field $Z$ . Two triples $(U,X,\varphi)$ and $(U,Y,\psi)$ are strongly isotopic if they are joined by a continuous path of such data.

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

\begin{gathered}(U,X)\ \text{hyperbolic plug with filling MS laminations},\ \Lambda\ \text{without attractors or repellers},\ \varphi\ \text{strongly transverse}\\ \Longrightarrow\ \exists\,(Y,\psi)\ \text{strongly isotopic to}\ (X,\varphi)\ \text{with the field induced by } Y \text{ on } U/\psi\ \text{Anosov}.\end{gathered}

Milestones

Proposition 1.1: gluing two hyperbolic plugs along transverse laminations gives a hyperbolic plug. Proposition 1.3: strongly transverse gluing preserves filling MS laminations.
Lemma 3.27 (self-gluing case): the glued manifold $U/\varphi$ exists as a closed smooth manifold with an induced vector field.
Proposition 1.6: if the graph of basic pieces is strongly connected, the Anosov flow of Theorem 1.5 is transitive.
Theorem 1.8: every transitive Anosov flow on a closed 3-manifold is a factor of a transitive Anosov flow on another closed 3-manifold, restricted to a compact invariant set.
Theorem 1.9: some closed orientable 3-manifold carries both a transitive and a nontransitive Anosov flow.
Theorem 1.10 and Corollary 1.11: every MS foliation of a closed orientable surface is the entrance foliation of a transitive attracting hyperbolic plug; in particular incoherent transitive hyperbolic attractors exist.
Theorem 1.12: every hyperbolic plug with filling MS laminations embeds, up to topological equivalence, in an Anosov flow on a closed orientable 3-manifold, which can be taken transitive when $\Lambda$ has no attractors or repellers.
Theorem 1.13: for every $n\ge1$ some closed orientable 3-manifold carries $n$ pairwise inequivalent transitive Anosov flows.
Theorem 1.15: some transitive Anosov flow admits infinitely many pairwise nonisotopic transverse tori.

Significance

Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.

Difficulty

The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on $\partial^{in}U$ are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing $\varphi$ and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).

Formalization scope

Manifolds are modelled on the half-space EuclideanHalfSpace 3 with a $C^\infty$ structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.
Vector fields are C¹ sections; flows are encoded by integral curves, so that partial flows on manifolds with boundary make sense; flowMap X t x is $x$ when the orbit is undefined.
Hyperbolicity is quantified over a continuous Riemannian metric, invariant line fields and constants $C,\lambda>0$ ; continuity of the splitting is not imposed (it is automatic).
Filling MS laminations are encoded through the strip condition (Lemma 3.21); leaves of $L^s$ are path components of intersections of weak stable manifolds with $\partial^{in}U$ .
The glued manifold $U/\varphi$ is not a quotient type: statements quantify over every closed smooth 3-manifold $N$ with a surjective C¹ immersion $q:U\to N$ realising the identification. Lemma 3.27 (a milestone) guarantees such $N$ exists, so these statements are not vacuous. The induced field is not required to be C¹ and "Anosov" there means hyperbolicity of the whole manifold.
Useful reusable infrastructure: flows of C¹ vector fields on compact manifolds (with boundary), stable manifold theory, the λ-lemma, laminations and foliations of surfaces, and gluing of manifolds along boundary components.

Selected references

F. Béguin, C. Bonatti, B. Yu, Building Anosov flows on 3-manifolds, Geom. Topol. 21 (2017) 1837–1930. https://doi.org/10.2140/gt.2017.21.1837

59 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: Lucas

Lindgren 2022: Dynamic-Programming Price Adjustment and Lyapunov StabilityResearch Paper

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$ , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$ , and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$ . Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$ ; the aggregate expenditure is

E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,

whose value function is $J(t,p)$ . The Hamiltonian (eq. (8)) is

H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$ , and the HJB equation (eq. (10)) reads

\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$ . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$ .

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$ , then on any interval $[t,T]$ on which

E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$ , it is strictly positive on $[t,T)$ .

Milestones

Eq. (4): under the normalization $\langle p,p\rangle=1$ , $\langle p,\dot p\rangle=0$ .
Eq. (9): for $m>0$ , $v$ minimizes $H$ if and only if $mv=-\nabla J$ .
Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .

Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$ .
Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$ .

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$ , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$ , $J=ap^2+cs$ , $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

8 thms2 active usersReviewed

Differential Geometry·Captain: Lucas

Pugh's Closing LemmaResearch Paper

Motivation

A periodic point of a map $f\colon M\to M$ is a point $x$ with $f^n(x)=x$ for some $n\ge 1$ . A nonwandering point is a much weaker form of recurrence: every neighbourhood $U$ of $x$ eventually returns to meet itself, $f^n(U)\cap U\ne\emptyset$ for some $n\ge 1$ . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to $x$ exactly.

Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if $x$ is nonwandering for a $C^1$ diffeomorphism $f$ of a compact manifold, then some diffeomorphism $g$ , as close to $f$ as desired in the $C^1$ topology, has $x$ as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a $C^1$ -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.

Setting

Let $M$ be a compact smooth manifold of dimension $d$ , Hausdorff and without boundary. Write $\mathrm{Diff}^1(M)$ for the set of $C^1$ diffeomorphisms $g\colon M\to M$ : bijections such that $g$ and $g^{-1}$ are continuously differentiable. For $g\in\mathrm{Diff}^1(M)$ , $Tg\colon TM\to TM$ denotes its tangent map on the tangent bundle.

The $C^1$ topology on $\mathrm{Diff}^1(M)$ is the coarsest topology for which $g\mapsto Tg$ is continuous, where the space $C(TM,TM)$ of continuous self-maps of $TM$ carries the compact-open topology. Two diffeomorphisms are $C^1$ -close when they, and their derivatives, are uniformly close.

For a map $h\colon X\to X$ of a topological space:

$x$ is nonwandering if for every neighbourhood $U$ of $x$ there is $n\ge 1$ with $h^n(U)\cap U\ne\emptyset$ ; the nonwandering set is $\Omega(h)$ ;
$\mathrm{Per}(h)=\{x : \exists\, n\ge 1,\ h^n(x)=x\}$ is the set of periodic points.

Formalization targets

Goal: Pugh's closing lemma

For every $f\in\mathrm{Diff}^1(M)$ and every $x\in\Omega(f)$ ,

\forall\ \mathcal U \text{ a } C^1\text{-neighbourhood of } f,\quad \exists\, g\in\mathcal U,\ \ x\in\mathrm{Per}(g).

Milestones

$\mathrm{Per}(f)\subseteq\Omega(f)$ for any map $f$ .
$\Omega(f)$ is closed for any map $f$ .
$f(\Omega(f))=\Omega(f)$ for a homeomorphism $f$ .
$\Omega(f)\ne\emptyset$ for any map of a nonempty compact space.
General Density Theorem (Pugh 1967): there is a residual set $\mathcal G\subseteq\mathrm{Diff}^1(M)$ with

\overline{\mathrm{Per}(g)}=\Omega(g)\qquad (g\in\mathcal G).

Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.

Significance

The result. The closing lemma turns a topological recurrence property into periodicity after a $C^1$ -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic $C^1$ diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of $C^1$ generic dynamics.

Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the $C^1$ topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.

Difficulty

The first idea is to take the returning piece of orbit near $x$ and push it back to $x$ with a small local perturbation. This fails in the $C^1$ topology. Moving a point by distance $\delta$ with a bump supported in a ball of radius $r$ costs $C^1$ size about $\delta/r$ , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be $C^1$ -small. The derivative $Df^n$ along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.

Formalization scope

$\mathrm{Diff}^1(M)$ and its $C^1$ topology come from the published definition file BCWCentralizer_Basic. $\mathrm{Diff}^1(M)$ is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by $g\mapsto Tg$ into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual $C^1$ topology.
"Compact smooth manifold": a Hausdorff compact space with a $C^\infty$ atlas modelled on $\mathbb R^d$ , so without boundary. $d$ is arbitrary.
"Arbitrarily close" means that every neighbourhood of $f$ in the $C^1$ topology contains a suitable $g$ . "Periodic" requires a period $n\ge 1$ . Allowing $n=0$ would make every point periodic and the statement trivial.
The perturbation $g$ is only required to be a $C^1$ diffeomorphism, matching $\mathrm{Diff}^1(M)$ in the source.
The nonwandering notion is the definition item PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.

Welcome contributions: a general theory of the $C^1$ topology on $\mathrm{Diff}^1(M)$ (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.

Selected references

C. C. Pugh, An Improved Closing Lemma and a General Density Theorem, American Journal of Mathematics 89 (4), 1967, 1010–1021. https://doi.org/10.2307/2373414
Wikipedia, Pugh's closing lemma, revision 1304222873. https://en.wikipedia.org/w/index.php?title=Pugh%27s_closing_lemma&oldid=1304222873
V. Araújo, M. J. Pacifico, Three-Dimensional Flows, Springer, 2010, ISBN 978-3-642-11414-4.

8 thms2 active usersReviewed

Captain: Lucas

The C¹-generic diffeomorphism has trivial centralizer (Bonatti–Crovisier–Wilkinson)Research Paper

Motivation

Two commuting diffeomorphisms $f,g$ of a manifold $M$ share all of their dynamics: $g$ permutes the orbits of $f$ and preserves every smooth and topological invariant of $f$ . The centralizer of $f\in\mathrm{Diff}^r(M)$ ,

Z^r(f)=\{g\in\mathrm{Diff}^r(M): fg=gf\},

always contains the cyclic group $\langle f\rangle=\{f^n:n\in\mathbb Z\}$ , and $f$ has trivial centralizer when $Z^r(f)=\langle f\rangle$ . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in $\mathrm{Diff}^r(M)$ (one of Smale's problems for the 21st century).

Timeline: Kopell (1970) answered the question for $r\ge2$ on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the $C^1$ topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in $\mathrm{Diff}^1(M)$ ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in $\mathrm{Diff}^1(M)$ for every compact manifold.

Setting

$M$ is a closed (compact, boundaryless), connected smooth manifold of dimension $d$ . $\mathrm{Diff}^1(M)$ is the space of $C^1$ diffeomorphisms of $M$ with the $C^1$ topology; a subset is residual if it contains a countable intersection of open dense sets.

Formalization targets

Goal (Main Theorem, p. 3)

There is a residual subset $\mathcal R\subset\mathrm{Diff}^1(M)$ such that for every $f\in\mathcal R$ and every $g\in\mathrm{Diff}^1(M)$ with $fg=gf$ , one has $g=f^n$ for some $n\in\mathbb Z$ .

Milestones

Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is $C^1$ -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when $\dim M\ge2$ ).

Significance

The theorem answers the second (and hence the first) part of Smale's question in the $C^1$ topology, and exhibits a precise link between dynamical properties of $f$ (large derivative and unbounded distortion) and the algebraic structure of $f$ inside the group $\mathrm{Diff}^1(M)$ . The result is proved in the literature; it has not been formalized.

Difficulty

The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.

Formalization scope

$M$ is a charted space over $\mathbb R^d$ with a $C^\infty$ atlas, Hausdorff, compact and connected; $\mathrm{Diff}^1(M)$ is Mathlib's type of $C^1$ diffeomorphisms. The $C^1$ topology is encoded as the topology induced by $f\mapsto Tf$ into the compact-open topology on continuous self-maps of the tangent bundle $TM$ . Powers $f^n$ , $n\in\mathbb Z$ , are taken in the permutation group of $M$ . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians $|\det Df^n|$ are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.

Contributions welcome: the $C^1$ topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.

Selected references

C. Bonatti, S. Crovisier, A. Wilkinson, The $C^1$ generic diffeomorphism has trivial centralizer, Publ. Math. IHÉS 109 (2009); arXiv:0804.1416. https://arxiv.org/abs/0804.1416
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998).
N. Kopell, Commuting diffeomorphisms, Proc. Sympos. Pure Math. 14 (1970).

7 thms2 active usersReviewed

Algebraic Geometry·Captain: Lucas

Albouy–Kaloshin: Finiteness of Planar Five-Body Central ConfigurationsResearch Paper

Motivation

A central configuration of the Newtonian $n$ -body problem is a placement of $n$ point masses in which the gravitational acceleration of every body points toward the centre of mass and is proportional to its distance from it. Central configurations generate the only explicitly known solutions of the $n$ -body problem (the homographic, or self-similar, motions), they are the possible limiting shapes of total collisions, and they organise the topology of the integral manifolds. Counting them is therefore a basic question of celestial mechanics.

Timeline.

Euler (1767) and Lagrange (1772) found all central configurations of three bodies: three collinear ones and the equilateral triangle.
Moulton (1910) showed there are exactly $n!/2$ collinear central configurations for any positive masses.
Chazy (1918) postulated that all central configurations are nondegenerate, which would imply finiteness; Wintner (1941) stated finiteness as a conjecture.
Palmore (1975) gave a degenerate example, refuting Chazy's postulate but not finiteness.
Smale (1998) listed finiteness of relative equilibria for every choice of positive masses as the 6th of his problems for the 21st century.
Hampton and Moeckel (2006) proved finiteness for $n = 4$ , using heavy computer algebra (BKK theory).
Albouy and Kaloshin (2012) gave a new proof for $n = 4$ that avoids heavy computation, and proved finiteness for $n = 5$ except possibly for masses in a codimension-2 algebraic subset of the mass space. The case $n \ge 6$ , and the $n = 5$ case for the excluded masses, remain open.

Setting

Fix $n$ bodies with masses $m_1,\dots,m_n$ ; body $k$ sits at $(x_k,y_k)\in\mathbb R^2$ . Write $x_{kl}=x_l-x_k$ , $y_{kl}=y_l-y_k$ and $r_{kl}=\sqrt{x_{kl}^2+y_{kl}^2}$ . A configuration with all $r_{kl}>0$ is a central configuration (normalised so that the proportionality constant is $1$ ) when, for every $k$ ,

\begin{pmatrix}x_k\\ y_k\end{pmatrix}=\sum_{l\ne k} m_l\, r_{kl}^{-3}\begin{pmatrix}x_k-x_l\\ y_k-y_l\end{pmatrix}.

These equations are invariant under rotations of the plane; imposing $y_{12}=0$ removes this freedom, and a solution with this normalisation is a positive normalized central configuration (Definition 1 of the paper; Lean: PosNormalizedCC n m).

The proof works in the complex domain. Introducing unknowns $\delta_{kl}$ (inverse distances) with $\delta_{kl}^2(x_{kl}^2+y_{kl}^2)=1$ turns the equations into the polynomial system (4) on $\mathbb C^{2n}\times\mathbb C^{n(n-1)/2}$ :

x_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(x_k-x_l),\qquad y_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(y_k-y_l),\qquad y_{12}=0 .

A complex solution is a normalized central configuration (Lean: NormalizedCC n m), a real one if all $x_k,y_k$ are real (Lean: RealNormalizedCC n m). The potential is $U=\sum_{k<l}m_km_l\delta_{kl}$ (Lean: potential n m).

Formalization targets

Goal — Theorem 2 (planar five bodies)

There is a closed algebraic subset $A\subset\mathbb R^5$ of codimension at least $2$ such that for all masses $m\in(\mathbb R_{>0})^5\setminus A$ ,

\#\{\text{positive normalized central configurations of the planar 5-body problem with masses } m\}<\infty .

The exceptional set is not made explicit; only its existence and dimension bound are asserted.

Stronger — Theorem 6

The same statement with all complex solutions of system (4) in place of the positive real ones.

Four bodies — Theorems 1, 3, 4, 5

For $n=4$ and every positive masses: finitely many positive (Theorem 1, Hampton–Moeckel) and even real (Theorem 5) normalized central configurations; finitely many complex ones unless the masses satisfy explicit polynomial relations (Theorem 3) or are all equal (Theorem 4).

Tools — Lemmas 1 and 2 and an explicit example

Lemma 1 (a polynomial image of an affine variety is finite or cofinite), Lemma 2 (the potential takes finitely many values on the solution set), and the explicit mass vector $(1,2,3,4,5)$ .

Significance

The result. Theorem 2 is the first finiteness result for planar central configurations of five bodies, settling Smale's 6th problem for $n=5$ for generic masses; before it, no single 5-tuple of positive masses was known to have finitely many planar central configurations. Its four-body part gives a short proof of the Hampton–Moeckel theorem, including the real (not necessarily positive) solutions.

Formalizing it. The results are proved on paper; none of them is formalized. A formal development requires affine elimination theory (Chevalley's theorem on constructible images in the form of Lemma 1), a Sard-type argument on algebraic sets (Lemma 2), and the singular-sequence analysis of Sections 3–9, which is a long case analysis of limiting diagrams together with polynomial eliminations done by computer algebra in the paper.

Difficulty

Finiteness is not a local statement: nondegeneracy fails in general (Palmore), so no implicit-function argument applies, and a continuum of solutions would have to be excluded globally. In the complex domain continua genuinely exist for some masses (Roberts' continuum with a negative mass; its sign-modified version with positive masses solves system (4)), so any proof must use the positivity of the masses in an essential way, and the exceptional mass set of Theorem 2 cannot simply be dropped with the present method.

Formalization scope

Bodies are indexed by Fin n; the paper's bodies $1$ and $2$ are the indices 0 and 1, so the normalisation reads y 1 - y 0 = 0.
Masses are real (and hypothesised positive) in all main theorems; in the definition of NormalizedCC they are complex, as in Section 2 of the paper. Lemma 2 carries the paper's standing hypothesis that no nonempty subset of bodies has total mass zero (NoZeroSubMass).
A point of system (4) is a triple (x, y, δ); δ is a full n × n array constrained to be symmetric with zero diagonal, so it carries exactly the $n(n-1)/2$ unknowns $\delta_{kl}$ , $k<l$ . Finiteness of the solution set is unaffected by this encoding.
"Closed algebraic subset of codimension 2 of the mass space" is encoded as the real zero locus massZeroLocus I of an ideal I of $\mathbb R[m_1,\dots,m_5]$ with ringKrullDim (ℝ[m] ⧸ I) ≤ 3. Taking $I=0$ is impossible (the quotient has dimension $5$ ), so the goal is not trivialised by an exceptional set equal to the whole mass space.
Finiteness is Set.Finite of the solution set.

Useful reusable infrastructure: finite-or-cofinite images of polynomial maps on affine varieties, and basic facts on central configurations (centre of mass, the identity $I=U$ ).

Selected references

A. Albouy, V. Kaloshin, Finiteness of central configurations of five bodies in the plane, Annals of Mathematics 176 (2012), 535–588. https://doi.org/10.4007/annals.2012.176.1.10
M. Hampton, R. Moeckel, Finiteness of relative equilibria of the four-body problem, Inventiones Mathematicae 163 (2006), 289–312. https://doi.org/10.1007/s00222-005-0461-0
S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/BF03025291

10 thms2 active usersReviewed

Control Theory Linear algebra·Captain: mikedeng1

Stabilization for a Perturbed Chain of Integrators in Prescribed Time I: Prescribed-Time Estimates for the Linear Time-Varying FeedbackResearch Paper

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$ . The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$ , uniform over a bounded range $\underline b\le b\le\bar b$ .
2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$ . Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$ , and let $J_n$ be the $n$ -th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$ . The perturbed chain of integrators is

\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$ . Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$ , the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$ . An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$ . It defines

\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.

The parameter $\lambda$ blows up at $T$ , and $s$ maps $[0,T)$ onto $[0,\infty)$ . In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$ , the system becomes

y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$ , that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$ .

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$ , there are $K$ and $C>0$ with

|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)

for every $\eta\ge1$ , every $b\ge\underline b$ , every disturbance $d$ , every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$ . Since $\lambda(t)\to\infty$ , every coordinate reaches $0$ at the prescribed time $T$ .

Milestones

§3 (10): $\dot\lambda = a\lambda^2$ , $\lambda$ is nondecreasing and tends to $\infty$ at $T$ , and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$ .
§3 (7)–(11): the transformed dynamics.
Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$ .
Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$ .
Proposition 12 (corrected): the ISS estimate (17) in the time $s$ .
Proposition 13: the $\eta$ -scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$ . The guarantee holds for every control gain $b\ge\underline b$ , however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$ , and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$ , reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$ . The standing assumptions are $n\ge1$ (§3), $T>0$ , $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$ , and $b\ge\underline b>0$ . No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

(17) as printed has no constant on the transient term and fails for $n\ge2$ : with $a\equiv1$ and $y(0)=e_1$ , $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
(23) as printed fails at $t=0$ whenever $\int_0^Ta<1$ . The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$ . The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$ , as on the page.
Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
" $\lambda$ increasing" is read as nondecreasing.
Corollary 14's " $t\ge0$ " is read as $t\in[0,T)$ .

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$ . Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$ , $K$ before $\eta$ , and $\rho,S,K$ before $b$ . No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

10 thms2 active usersReviewed

Probability Reinforcement Learning Stochastic Systems·Captain: mikedeng1

The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning I: Stability and Almost-Sure Convergence under Tapering StepsizesResearch Paper

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.

The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).

Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.

Setting

Fix $d\ge 0$ and work in $\mathbb R^d$ with the Euclidean norm. Let $h:\mathbb R^d\to\mathbb R^d$ and let $\{a(n)\}_{n\ge0}$ be a deterministic sequence of positive step sizes. On a probability space $(\Omega,\mathcal F,\mathsf P)$ , random vectors $X(n)$ and $M(n)$ satisfy the stochastic approximation recursion

X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n\ge0. \tag{1.1}

Its mean ODE is $\dot x = h(x)$ (1.2). For $r>0$ the scaled field is $h_r(x)=h(rx)/r$ , with the scaled ODE $\dot x = h_r(x)$ (1.4).

(A1) $h$ is Lipschitz; $h_r(x)\to h_\infty(x)$ as $r\to\infty$ for every $x$ ; and the origin is an asymptotically stable equilibrium of the fluid-limit ODE $\dot x = h_\infty(x)$ (1.5).
(A2) With $\mathcal F_n$ the history of the iterates up to time $n$ , $\{M(n)\}$ is a martingale difference sequence, $\mathsf E[M(n+1)\mid\mathcal F_n]=0$ , and for some constant $C_0<\infty$ , $\mathsf E[\|M(n+1)\|^2\mid\mathcal F_n]\le C_0(1+\|X(n)\|^2)$ .
(TS) Tapering step sizes: $0<a(n)\le1$ , $\sum_n a(n)=\infty$ , $\sum_n a(n)^2<\infty$ .

A point $x^*$ is globally asymptotically stable for $\dot x = h(x)$ if it is a Lyapunov-stable equilibrium and every solution converges to it.

Formalization targets

Goal: Theorem 2.2 (almost sure convergence)

Under (A1), (A2) and (TS), if $\dot x=h(x)$ has a unique globally asymptotically stable equilibrium $x^*$ , then for every initial condition $X(0)\in\mathbb R^d$ ,

X(n)\longrightarrow x^* \qquad \text{almost surely.}

The goal contains no constants and no rates, only the qualitative conclusion.

Milestone: Theorem 2.1 (i) (almost sure boundedness)

Under (A1), (A2) and (TS), for every initial condition,

\sup_n \|X(n)\| < \infty \qquad \text{almost surely.}

Milestones: the lemmas of Section 4.1

Lemma 4.1: the fluid-limit ODE is globally exponentially asymptotically stable.
Lemma 4.2: the piecewise ODE solutions $\hat\phi$ , $\phi^\infty$ used for comparison are bounded by a constant independent of the initial condition.
Lemma 4.3 (i), (ii): two discrete Bellman–Gronwall inequalities.
Lemma 4.4: for large scale $r$ , every solution of $\dot x = h_r(x)$ from the unit ball is $\epsilon$ -small on a window $[T,T+1]$ .
Lemma 4.5: the rescaled iterates have uniformly bounded second moments, and the rescaled noise sum $\xi$ is an $L^2$ -bounded martingale.
Lemma 4.6: almost surely the rescaled interpolated iterates $\phi$ track $\hat\phi$ and stay bounded.

Significance

The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to $x^*$ with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.

Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of $h_r$ to $h_\infty$ on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.

Difficulty

The obvious approach is to compare the iterates with solutions of $\dot x = h(x)$ over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with $\|X(n)\|$ , so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.

A second difficulty is that the hypothesis (A1) concerns only the fluid limit $h_\infty$ , which describes the drift at infinite scale. It says nothing directly about $h$ at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit $r\to\infty$ to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued $L^2$ martingale convergence argument, none of which is available off the shelf for this setting.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on $[0,\infty)$ : the derivative is taken within $[0,\infty)$ at each $t\ge0$ , which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form $\|x(t)-x^*\|\le b e^{-\delta t}\|x(0)-x^*\|$ ). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.

The filtration in (A2) is the natural filtration of the iterates. Because $a(n)>0$ , it carries the same information as the paper's $\sigma(X(i),M(i),i\le n)$ . (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ , so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. " $\sup_n\|X(n)\|<\infty$ " is boundedness above of the set of norms, not a real supremum, which Lean sets to $0$ on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in $[0,\infty]$ .

The proof objects of Section 4.1 (time grid $t(n)$ , blocks $m(j)$ and $T(j)$ , scales $r(j)$ , the interpolation $\phi$ , the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions $\hat\phi$ and $\phi^\infty$ are characterized by a predicate, and the lemmas hold for every function satisfying it.

Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of $h_r$ on compact sets, the discrete Gronwall lemmas, and $L^2$ -bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.

Selected references

V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
L. Ljung, Analysis of Recursive Stochastic Algorithms, IEEE Trans. Automat. Control 22(4):551–575, 1977. https://doi.org/10.1109/TAC.1977.1101561
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
J. G. Dai, On Positive Harris Recurrence of Multiclass Queueing Networks: A Unified Approach via Fluid Limit Models, Ann. Appl. Probab. 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
J. G. Dai and S. P. Meyn, Stability and Convergence of Moments for Multiclass Queueing Networks via Fluid Limit Models, IEEE Trans. Automat. Control 40(11):1889–1904, 1995. https://doi.org/10.1109/9.471210
V. S. Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint, Cambridge University Press / Hindustan Book Agency, 2008. https://doi.org/10.1007/978-93-86279-38-5

17 thms2 active usersReviewed

Missions

Fast Convergence of Inertial Dynamics and Algorithms with Asymptotic Vanishing Viscosity 2: For Strongly Convex Φ and α > 3, Φ(x(t)) − min Φ, ‖x(t) − x*‖² and ‖ẋ(t)‖² Are O(t^(−2α/3))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4 (p. 11)

Milestones (explicit forms, valid for t≥t1t\ge t_1t≥t1​)

Significance

Difficulty

Formalization scope

Selected references

Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators 2: λ₂(L(P_ij cos φ_ij)) > λ_critical Gives Phase Cohesiveness and Exponential Frequency SynchronizationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem V.5 (Synchronization condition II)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators 1: Γ_min > Γ_critical Gives Phase Cohesiveness and Exponential Frequency SynchronizationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem V.3 (Synchronization condition I), corrected

Milestones

Significance

Difficulty

Formalization scope

Selected references

Ergodicity of triangular billiards with an irrational angleResearch Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Theorem 1

Significance

Difficulty

Formalization scope

Selected references

Boundedness and persistence of weakly reversible mass-action systemsResearch Paper

Motivation: can a weakly reversible reaction network lose a species or blow up?

Timeline

Setting

Formalization targets

Goal: global existence, boundedness and persistence (Theorem 1.1)

Significance

Difficulty

Formalization scope

Selected references

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 1: Near the Two-Player Unit-Disk Game Γ₀ of Section II, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

Setting

Formalization targets

Goal: THEOREM 1 for the game Γ0\Gamma_0Γ0​ of §II

Milestones

Significance

Difficulty

Formalization scope

Selected references

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 2: Near Jordan's Three-Player Game Γ₀ of Section III, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 near Jordan's game

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Power of Two Choices in Randomized Load Balancing I: In the Limiting Supermarket System the Expected Time Converges to T_d(λ) = Σ λ^((d^i−d)/(d−1))Research Paper

Motivation

Setting

Formalization targets

Goal: Corollary 2

Milestones, in the order the proof uses them

Significance

Difficulty

Milestones (explicit forms, valid for $t\ge t_1$ )

Goal: THEOREM 1 for the game $\Gamma_0$ of §II