Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing steps $\gamma_n$ and noise $U_n$. Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics $\dot x=F(x)$. Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of $F$ (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.

The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set $\Lambda$ and is constant on $\Lambda$. Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into $\Lambda$. It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.

Timeline.

• Conley (Isolated Invariant Sets and the Morse Index, CBMS 38, 1978) introduced chain recurrence and the attractor–repeller description of it.
• Benaïm and Hirsch (J. Dyn. Diff. Eq. 8, 1996) identified limit sets of asymptotic pseudotrajectories with internally chain transitive sets.
• Benaïm (SIAM J. Control Optim. 34, 1996) developed the dynamical-systems approach to stochastic approximation built on these notions.
• Bowen (J. Differential Equations 18, 1975) characterized chain transitivity by the absence of proper attractors, the content of Proposition 5.3 of the notes.
• The 1999 notes state the Lyapounov criterion in the form used here, for semiflows on arbitrary metric spaces.

Setting

Let $(M,d)$ be a metric space, with no compactness or completeness assumed. 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$. For an invariant $\Lambda$, the restriction $\Phi|\Lambda$ is the semiflow $\Phi$ acting on $\Lambda$.
• For $\delta,T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ is a list of points $y_0,\dots,y_k$ ($k\ge1$) 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$.
• A set $L$ is internally chain transitive if it is nonempty, compact and invariant, and for all $a,b\in L$ and all $\delta,T>0$ there is a $(\delta,T)$-pseudo-orbit of $\Phi|L$, so with every $y_i\in L$, from $a$ to $b$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\mathrm{dist}(\Phi_t x,A)\to0$ uniformly. Its basin is the set of points $x$ with $\mathrm{dist}(\Phi_t x,A)\to0$.
• Let $\Lambda\subset M$ be compact and invariant. A continuous $V:M\to\mathbb R$ is a Lyapounov function for $\Lambda$ if $t\mapsto V(\Phi_t(x))$ is constant for $x\in\Lambda$ and strictly decreasing for $x\notin\Lambda$.

Formalization targets

Goal: Proposition 6.4

Let $\Lambda$ be compact invariant and $V$ a Lyapounov function for $\Lambda$, and assume that $V(\Lambda)$ has empty interior in $\mathbb R$. Then for every internally chain transitive set $L$,

$$L\subset\Lambda\qquad\text{and}\qquad V|_L\ \text{is constant}.$$

Milestones

1. Lemma 5.2. If $U$ is open with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$, there is an attractor $A\subset U$ whose basin contains $\overline U$.
2. 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.
3. The claim of the proof of 6.4. For $L$ internally chain transitive and $v^*=\inf_L V$: $L\cap\Lambda\ne\emptyset$ and $v^*=\inf_{L\cap\Lambda}V$.
4. The sublevel step of the proof of 6.4. For every $c>v^*$ with $c\notin V(\Lambda)$, $V<c$ on all of $L$.

Significance

The result. Proposition 6.4 converts a statement about real numbers, that $V(\Lambda)$ has empty interior, into a statement about dynamics: the chain recurrent behaviour of $\Phi$ is confined to $\Lambda$. With Theorem 5.7 it gives the following. If $\Phi$ has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in $\Lambda$, and $V$ is constant on it. When $\Lambda$ is the set of equilibria and $V(\Lambda)$ is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.

Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:

• a formal definition layer for these notions on Mathlib's Flow;
• formal proofs of Lemma 5.2 and Proposition 5.3, which are reused across this series (missions 1 and 6);
• the Lyapounov criterion itself.

Difficulty

The obvious argument does not work. It runs: $V$ decreases along trajectories, so along an orbit in $L$ the value of $V$ must settle on $\Lambda$. But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the $k$ jumps, $V$ may increase by an amount that is small but not controlled in number, so monotonicity of $V$ along true trajectories says nothing directly about $L$. Remark 6.5 shows that the conclusion is genuinely false without a condition on $V(\Lambda)$. The difficulty is therefore global: pseudo-orbits that climb back up $V$ through many small jumps must be excluded using information about the restricted semiflow $\Phi|L$ as a whole, not the monotonicity of $V$ along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.

Formalization scope

• Representation. $M$ is any MetricSpace, and the semiflow is Flow ℝ≥0 M.
• Invariance is equality $\Phi_t(A)=A$ for every $t$, not inclusion.
• Pseudo-orbits have at least one trajectory piece ($k\ge1$), times $\ge T$, an exact endpoint, and, in the internal notions, all their points in the set.
• Nonemptiness. Internally chain transitive and internally chain recurrent sets are nonempty by definition. Accordingly, Proposition 5.3 assumes $\Lambda\neq\emptyset$ and Lemma 5.2 assumes $U\neq\emptyset$.
• Lyapounov function. The predicate contains the standing assumptions of its definition: $\Lambda$ is compact and invariant, $V$ is continuous, $V(\Phi_t x)=V(x)$ on $\Lambda$, and $t\mapsto V(\Phi_t x)$ is strictly antitone off $\Lambda$.
• Empty interior is interior (V '' Λ) = ∅ in $\mathbb R$, not countability, finiteness or measure zero.
• Infima are stated with IsGLB, not a real sInf.

The following formalizations are trivializing and are excluded:

• chains with no jumps, under which every point is chain recurrent;
• invariance as inclusion;
• a non-strict decrease condition, under which constant functions are Lyapounov functions and the goal is false;
• chains of $\Phi$ that leave $L$, a strictly weaker notion;
• quantifying only over limit sets instead of every internally chain transitive set.

A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction $A=\bigcap_{t\ge0}\overline{\bigcup_{s\ge t}\Phi_s(U)}$ and the open sets $\{y: x\hookrightarrow_{\delta,T}y\}$ used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, 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. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218613
• 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
• R. Bowen, ω-limit sets for Axiom A diffeomorphisms, J. Differential Equations 18 (1975), 333–339. https://doi.org/10.1016/0022-0396(75)90065-0

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

• Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
• Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
• Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

• Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ($k\in\mathcal J$), service times $v_k^i>0$, and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$. When the $i$th customer served at station $k$ finishes, it moves to station $\phi_k^i$, or leaves if $\phi_k^i=0$. The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$, the service-time variances $s_k=\operatorname{var} v_k^1$, the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$), and the interarrival variances $a_k=\operatorname{var} u_k^1$. The routing matrix $P=(p_{kj})$, $p_{kj}=P\{\phi_k^1=j\}$, has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$, and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$, with $e_0=0$. The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

$$Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .$$

A sequence of such networks, indexed by $n$, shares $K$, $\mathcal J$ and $P$. Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$. With $\nu(n)=\lambda(n)+\mu(n)P$, the heavy-traffic condition is

$$c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .$$

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$. The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$, $0\le t\le1$.

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$, where

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$. Then

$$Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.$$

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

• the existence and uniqueness claim for (1)–(3);
• the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
• the least-element map $f$ (Proposition 1);
• the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
• the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
• stochastic boundedness of $Z^n$ (Lemma 6);
• vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
• the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

• a formal statement of the network, of its Harrison representation, and of weak convergence in $D$;
• a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
• eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$, which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$. It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

• Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
• A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$.
• The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
• "Spectral radius $<1$" is stated as $P^m\to0$.
• $(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
• The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$, (22) and (26) over $k\in\mathcal J$, and $\mathcal J$ is the same for all $n$.
• Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$. It is defined by continuity, $\xi(0)=0$, independent increments, and the Gaussian characteristic function of increments.
• $Z$ is the reflection of $\xi$ in the sense of (14)–(17).
• Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J$_1$ convergence on $[0,1]$. This form accommodates a separate probability space for each $n$.

Added hypotheses, each implicit on the page:

1. The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
2. Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

• convergence of finite-dimensional distributions only;
• a single network without the index $n$;
• uniform convergence used in place of the Skorohod topology without the coupling;
• a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

• the deterministic reflection-map results;
• Donsker-type theorems for renewal counting processes in $D$;
• the random time-change lemma (Billingsley);
• the continuous mapping theorem in coupling form.

Selected references

• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
• J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
• J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
• D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
• P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

Motivation

The single-server queue with general independent interarrival and service times, the G/G/1 queue, is the basic model of a congested resource: a machine, a link, a checkout. For Markovian arrivals or services the mean wait has a closed form (the Pollaczek–Khintchine formula for M/G/1, the geometric law for G/M/1). For general distributions it has none, and the mean wait depends on the whole distributions of the interarrival and service times, not only on their moments. Capacity planning still needs numbers. Bounds that use only the first two moments are therefore the practical tool. They say how bad congestion can be for any queue with a given arrival rate, service rate and variabilities, and they become exact as the traffic intensity approaches one.

This mission formalizes Chapter 7, §7.1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), together with the heavy-traffic Theorem 7.1 of §7.2.3.

Timeline. Lindley (Proc. Cambridge Philos. Soc., 1952) derived the recursion for successive waiting times and characterized the stationary law. Kingman (Proc. Cambridge Philos. Soc., 1961, 1962) proved the heavy-traffic exponential limit. In "Some inequalities for the queue GI/G/1" (Biometrika, 1962) he proved the two-moment upper bound. Marshall (1968) derived further moment relations and bounds (Operations Research, 1968). Marchal (Operations Research, 1978) gave the lower bound (7.14).

Setting

A G/G/1 queue is specified by two probability laws on $[0,\infty)$: the law $A$ of an interarrival time $T$ and the law $B$ of a service time $S$. Both have finite second moments, and

$$E[T] = \frac1\lambda,\quad E[S] = \frac1\mu,\quad \sigma_A^2 = \mathrm{Var}[T],\quad \sigma_B^2 = \mathrm{Var}[S],\quad \rho = \frac{\lambda}{\mu}.$$

The pairs $(S^{(n)}, T^{(n)})$ are independent and identically distributed, and $S^{(n)}$ is independent of $T^{(n)}$. Customers are served first come, first served. The line delay $W_q^{(n)}$ of the $n$th customer obeys Lindley's recursion

$$W_q^{(n+1)} = \max\bigl(0,\ W_q^{(n)} + U^{(n)}\bigr), \qquad U^{(n)} = S^{(n)} - T^{(n)}, \tag{7.1}$$

and $W_q^{(n)}$ is independent of $(S^{(n)}, T^{(n)})$. The idle gap $X^{(n)} = -\min(0, W_q^{(n)} + U^{(n)})$ is the time between the $n$th departure and the next start of service.

The queue is stationary when the law $\nu$ of $W_q^{(n)}$ does not depend on $n$, that is, when one step of (7.1) maps $\nu$ to itself. The mean stationary line delay is $W_q = E[W_q^{(n)}] = \int w\,d\nu(w)$. In the Lean development these objects are IsGG1Input A B lam mu, lindley, idleX, IsStationaryWaitLaw A B ν and meanWait ν, in the namespace QueueingFundamentals.Bounds.

Formalization targets

Goal: Kingman's upper bound (7.13)

For every stationary G/G/1 queue with $\rho < 1$, $W_q$ is finite and

$$W_q \le \frac{\lambda(\sigma_A^2 + \sigma_B^2)}{2(1-\rho)}.$$

Milestones

• the idle-gap identity $E[X] = -E[U] = 1/\lambda - 1/\mu$ (7.4), and the mean-wait formula (7.7)

$$W_q = \frac{E[X^2] - E[U^2]}{2E[U]};$$

• the variance of the interdeparture time $D = S^{(n+1)} + X^{(n)}$ (7.12): $\mathrm{Var}[D] = 2\sigma_B^2 + \sigma_A^2 - 2W_q(1/\lambda - 1/\mu)$;
• Marchal's lower bound (7.14), $W_q \ge (\lambda^2\sigma_B^2 + \rho(\rho-2))/(2\lambda(1-\rho))$;
• the distributional lower bound $W_q \ge r_0$, with $r_0$ the unique nonnegative root of $f(z) = z - \int_{-z}^\infty [1 - U(t)]\,dt$ and $U(t)$ the CDF of $S - T$ ((7.15), (7.16));
• the two-sided estimate (7.17), $\max\bigl(0, r_0, \tfrac{\lambda^2\sigma_B^2 + \rho(\rho-2)}{2\lambda(1-\rho)}\bigr) \le W_q \le \tfrac{\lambda(\sigma_A^2+\sigma_B^2)}{2(1-\rho)}$;
• Theorem 7.1 (heavy traffic): for a sequence of G/G/1 queues with $\rho_j \to 1$, $\alpha_j = -E[S_j - T_j]$ and $\beta_j^2 = \mathrm{Var}[S_j - T_j]$, under convergence of the input laws, $\mathrm{Var}[S - T] > 0$ and uniformly bounded $(2+\delta)$-moments,

$$\frac{2\alpha_j}{\beta_j^2}\,W_{q,j} \xrightarrow{d} \mathrm{Exp}(1).$$

The goal is (7.13) rather than the stronger (7.17) because it depends only on the first two moments of the input.

Significance

Kingman's bound is the most widely used performance estimate for single-server queues. It needs no distributional form, only two means and two variances. It yields the "Kingman formula" approximation used across manufacturing and service operations, and it is asymptotically exact as $\rho \to 1$ (Theorem 7.1). The departure variance (7.12) drives the decomposition approximations for networks of §7.3. The heavy-traffic theorem is the entry point to diffusion approximations of queues.

All results here are proved in the literature (Theorem 7.1 is stated in the book without proof). This mission produces the first machine-checked versions. As far as a search of the platform shows, none of these statements, and no stationary Lindley recursion, has been formalized. The substrate it needs is reusable for any mission on G/G/1, G/G/c or random walks: stationary laws of a recursion on distributions, moment identities for $\max(0,\cdot)$, and convergence in distribution.

Difficulty

The book's derivation squares (7.3) and takes expectations, using $E[(W_q^{(n+1)})^2] = E[(W_q^{(n)})^2]$. That step is valid only if the stationary wait has a finite second moment. It is not assumed here and fails in general: with finite second moments of $S$ and $T$ the stationary wait has a finite mean, but its second moment is finite only if $E[S^3] < \infty$. So the moment identity (7.7) cannot be obtained by cancelling second moments. A truncation or limiting argument is needed, and even the finiteness of $W_q$ has to be proved rather than assumed. The lower bound $W_q \ge r_0$ further needs a Jensen argument for the conditional mean of one Lindley step. Theorem 7.1 needs a uniform-integrability argument across a sequence of queues.

Formalization scope

Conventions committed to in Lean:

• laws, not random variables: $A$, $B$ and the stationary law $\nu$ are Measure ℝ; independence of $W_q^{(n)}, S^{(n)}, T^{(n)}$ (and $S^{(n+1)}$ for $D$) is the product measure;
• the input laws are probability measures on $[0,\infty)$ with finite second moments (MemLp id 2), $E[T] = 1/\lambda$, $E[S] = 1/\mu$, $\lambda, \mu > 0$, $\rho = \lambda/\mu < 1$;
• stationarity is invariance of the whole law $\nu$ under one step of (7.1), not equality of means;
• $W_q$, the variances (Mathlib variance) and $f_1$ are Lebesgue integrals. Every theorem therefore asserts, as part of its conclusion, that $\nu$ has a finite mean, and none assumes a finite second moment of $\nu$;
• $U(t)$ is Mathlib's cdf of the law of $S - T$;
• convergence in distribution is convergence of $\int g$ for all bounded continuous $g$, and $\mathrm{Exp}(1)$ is expMeasure 1.

Closed forms carried by the statements: (7.4), (7.7), (7.12), (7.13), (7.14) and (7.17) exactly as printed, and the scaling $2\alpha_j/\beta_j^2$ of Theorem 7.1.

Stating (7.13) with $W_q$, $E[X^2]$ or the idle probability as free real numbers constrained by (7.7) would reduce it to algebra. Here $W_q$ is always the mean of a stationary law of the queue.

Not formalized: (7.5) and (7.8), which need the idle-period law $I$ and the arrival-point probability $q_0$ as separate objects, and the multiserver bounds of §7.1.3. Proofs of any milestone are welcome, as are reusable lemmas on stationary laws of Lindley's recursion (existence, uniqueness, and finiteness of the mean under $E[S^2] < \infty$).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• D. V. Lindley, The theory of queues with a single server, Math. Proc. Cambridge Philos. Soc. 48 (1952)
• J. F. C. Kingman, The single server queue in heavy traffic, Math. Proc. Cambridge Philos. Soc. 57 (1961)
• J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49 (1962)
• K. T. Marshall, Some inequalities in queuing, Operations Research 16 (1968)
• W. G. Marchal, Some simpler bounds on the mean queuing time, Operations Research 26 (1978)

Motivation

Many service systems route several classes of work to servers with overlapping skills: call centers with cross-trained agents, manufacturing cells with flexible machines, computing clusters with heterogeneous processors. Choosing which server works on which class at each moment is a dynamic scheduling problem. Exact optimal policies are out of reach except in toy cases, so heavy-traffic theory replaces the queueing system by a Brownian control problem, solves that limit problem, and then asks for a policy in the original system whose performance converges to the Brownian optimum. This programme was proposed by Harrison (Harrison 1988), and the parallel server system studied here is the example Harrison used (Harrison, Ann. Appl. Probab. 1998) to show that the greedy static priority rule can be very inefficient.

Bell and Williams (2001) gave the first proof of asymptotic optimality of a continuous-review policy for this system, with renewal arrivals and general service times. Harrison (1998) had treated Poisson arrivals and deterministic service times with a discrete-review policy and a pathwise criterion. Harrison and López (Queueing Systems, 1999) identified the complete resource pooling condition for general parallel server systems. The threshold policy and the proof method of Bell and Williams were later extended to multiserver systems (Bell and Williams, Electron. J. Probab., 2005).

Setting

There are two job classes and two servers. Server 1 serves class 1 (activity 1); server 2 serves class 1 (activity 2) and class 2 (activity 3). A sequence of such systems is indexed by $r\to\infty$. On a probability space, i.i.d. sequences $\check u_k(i)$ ($k=1,2$) and $\check v_j(i)$ ($j=1,2,3$), $i\ge1$, are fixed: strictly positive, mutually independent, with mean one and finite variances $\alpha_k^2,\beta_j^2$. In system $r$ the interarrival times are $u_k^r(i)=\check u_k(i)/\lambda_k^r$ and the service times are $v_j^r(i)=\check v_j(i)/\mu_j^r$. The renewal processes $A_k^r(t)$ and $S_j^r(t)$ count arrivals and potential service completions.

A scheduling control policy is an allocation $T=(T_1,T_2,T_3)$, where $T_j(t)$ is the time devoted to activity $j$ in $[0,t]$. Each $T_j(t)$ is a random variable, each $T_j$ is continuous and nondecreasing from $0$, and so are the idle times $I_1=t-T_1$ and $I_2=t-T_2-T_3$. The queue lengths

$$Q_1(t)=A_1(t)-S_1(T_1(t))-S_2(T_2(t)),\qquad Q_2(t)=A_2(t)-S_3(T_3(t))$$

must be nonnegative. Policies may anticipate the future. The rates satisfy Assumption 3.1: $\lambda_1>\mu_1$, $1-(\lambda_1-\mu_1)/\mu_2=\lambda_2/\mu_3$, and the rates converge at rate $1/r$ to limits with second-order parameters $\theta_1,\theta_2$. Assumption 3.2 is $h_1\mu_2\ge h_2\mu_3$, and Assumption 3.3 gives finite exponential moments near $0$. With $\hat Q^r(t)=r^{-1}Q^r(r^2t)$ the cost is

$$\hat J^r(T^r)=\mathbf E\Big(\int_0^\infty e^{-\gamma t}\,h\cdot\hat Q^r(t)\,dt\Big).$$

The threshold policy with $L^r=[c\log r]$ works as follows. Server 1 works whenever it has a class 1 job available. Server 2 serves class 1 with preemptive-resume priority when more than $L^r$ class 1 jobs are present, and otherwise serves class 2. The Brownian benchmark is built from a two-dimensional Brownian motion $\tilde X$ with drift $\theta$ and diagonal covariance, from $y=(1,\mu_2/\mu_3)$, and from the reflected process $\tilde W^*=y\cdot\tilde X+\tilde V^*$ with $\tilde V^*(t)=-\inf_{s\le t}y\cdot\tilde X(s)$. Its cost is $J^*=\mathbf E\int_0^\infty e^{-\gamma t}h_2\,\tilde W^*(t)/y_2\,dt$.

Formalization targets

Goal: Theorem 5.3

For $c$ larger than a constant $c_0$ that depends only on the model data, and for every sequence $\{T^r\}$ of scheduling control policies,

$$\liminf_{r\to\infty}\hat J^r(T^r)\ \ge\ J^*\ =\ \lim_{r\to\infty}\hat J^r(T^{r,*}),\qquad J^*<\infty .$$

Milestones

• Proposition B.1: the one-dimensional Skorokhod problem, its explicit solution and its minimality.
• Appendix A, (181) and (184): Cramér-type deviation bounds for delayed renewal processes.
• Theorem 7.2: after first reaching $L^r$, the class 1 queue stays within $L^r-1$ of the threshold, with probability tending to one.
• Theorem 7.1: $(\hat Q_1^r,\hat I_1^r)\Rightarrow(0,0)$ under the threshold policy.
• Lemma 8.1: the fluid-scaled threshold allocations converge to $\bar T^*(t)=(t,\frac{\lambda_1-\mu_1}{\mu_2}t,\frac{\lambda_2}{\mu_3}t)$.
• Theorem 5.2 (state-space collapse): $(\hat Q_1^r,\hat Q_2^r,\hat I_1^r,\hat I_2^r)\Rightarrow(0,\tilde Q_2^*,0,\tilde I_2^*)$.
• Lemma 9.3: along a subsequence achieving a finite $\liminf$ cost, the fluid-scaled processes converge to $(0,\lambda t,\mu t,\bar T^*,0)$.

A further draft theorem states that Definition 5.1 determines an admissible allocation, unique pathwise, whenever $L^r\ge1$.

Significance

The theorem proves that a simple state-dependent rule, which sends server 2 to class 1 only when the class 1 queue exceeds a logarithmic safety stock, is asymptotically optimal among all policies, including those that anticipate the future. The limiting cost is the explicit optimum of the Brownian control problem. The proof gives a template for heavy-traffic asymptotic optimality under complete resource pooling: a lower bound valid for every policy, and state-space collapse under the proposed policy. The residual process analysis of Section 7 shows how a threshold of order $\log r$ makes starvation of server 1 negligible on the diffusion time scale.

The paper's results are proved but not machine-checked; no formal proof exists in any proof assistant. The mission asks for formal statements of the paper's main theorem and its supporting lemmas, followed by formal proofs. Parts of the development are independent of the paper: the one-dimensional Skorokhod map, renewal large deviation bounds, and convergence encodings on path space.

Difficulty

The lower bound must hold for arbitrary, possibly anticipating, policies, so no Markov structure is available. The argument has to pass through fluid limits of an arbitrary cost-minimizing subsequence and a pathwise minimality property, and Fatou's lemma for the limit needs uniform control. For the upper bound, the obvious approach, a static priority rule, is known to fail: it starves server 1 and produces a large class 1 queue. With a threshold policy, the hard step is to show that the class 1 queue, once at the threshold, rarely moves $L^r-1$ away from it over a time interval of length $r^2t$. That requires large deviation estimates for renewal processes started at random, multiparameter stopping times. Showing that $\hat J^r(T^{r,*})$ converges to $J^*$, rather than only that the processes converge in distribution, also requires uniform integrability of the scaled queue lengths.

Formalization scope

Classes and activities are indexed by Fin 2 and Fin 3. The i.i.d. sequences keep the paper's index base $i\ge1$, and the systems are indexed by $n\in\mathbb N$ with $r=r_n\in[1,\infty)$, $r_n\to\infty$. Time is real, and every condition is imposed for $t\ge0$. Admissibility is exactly (11)–(14). Measurability in (11) is with respect to the completion of $\mathbf P$, since the paper's space is complete. Finiteness of the renewal processes everywhere on $\Omega$, which the paper obtains by discarding a null set, is a hypothesis. Queue lengths are real, costs are lower Lebesgue integrals in $[0,\infty]$, counting processes take values in $\mathbb N\cup\{\infty\}$, and $\Lambda$, $\Lambda^*$ take values in the extended reals.

The constant $c_0$ is existential and is chosen after the model data and before $c$, the policies and the Brownian motions. The threshold relations are required only for the systems with $L^r\ge1$, which are all but finitely many. Each convergence to a deterministic limit (Theorem 7.1, Lemmas 8.1 and 9.3) is stated as u.o.c. convergence in probability, the paper's own equivalence (p. 633). Theorem 5.2 is stated in coupling form: there are copies of the processes on one probability space, with Skorokhod paths and the same laws, that converge almost surely uniformly on compacts. This is equivalent to weak convergence in $\mathbf D^4$ to a limit with continuous paths. $J^*$ is defined by (44) from an arbitrary pair of independent standard Brownian motions (Mathlib's IsBrownianReal), not by a closed form.

Two formalizations would make the goal trivial, and both are excluded. Leaving out the requirement that $T^{r,*}$ actually follow the policy would make the goal false or empty. Narrowing the class of competing policies, for example to non-anticipating ones, would weaken the theorem. A draft theorem also states that the threshold allocation exists and is unique pathwise, so the hypothesis on $T^{r,*}$ can be satisfied.

The development needs renewal theory (functional central limit theorems, Cramér bounds), multiparameter stopping times, tightness in $\mathbf D$, the Skorokhod representation theorem, the reflection map, and properties of reflected Brownian motion. Contributions are welcome at every level: proofs of milestones, reusable lemmas on renewal processes and the Skorokhod map, and further lemmas of the paper (Lemmas 7.5, 7.6 and 9.2 are not yet stated).

Selected references

• S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11 (2001) 608–649. https://doi.org/10.1214/aoap/1015345343
• J. M. Harrison, Heavy traffic analysis of a system with parallel servers: asymptotic optimality of discrete-review policies, Ann. Appl. Probab. 8 (1998) 822–848.
• J. M. Harrison and M. J. López, Heavy traffic resource pooling in parallel-server systems, Queueing Systems 33 (1999) 339–368.
• J. M. Harrison, Brownian models of queueing networks with heterogeneous customer populations, in Stochastic Differential Systems, Stochastic Control Theory and Their Applications, Springer (1988) 147–186.
• S. L. Bell and R. J. Williams, Dynamic scheduling of a parallel server system in heavy traffic with complete resource pooling: asymptotic optimality of a threshold policy, Electron. J. Probab. 10 (2005) 1044–1115.
• J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley (1985).

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

1. 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$;
2. 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

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

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

1. Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$.
2. A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$.
3. 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.
4. 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)$.
5. 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