Stochastic Systems

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem

$$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$

On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

Why reversibility

A stochastic process is reversible when a film of it run backwards is statistically indistinguishable from the film run forwards. For Markov processes in equilibrium this distributional symmetry has an algebraic counterpart, the detailed balance conditions, and that counterpart is what makes large classes of queueing networks, migration processes, loss networks, clustering processes and population-genetics models solvable in closed form. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) builds the whole theory of product-form equilibria on this link, and Chapter 1 sets it up.

The criterion that bears Kolmogorov's name goes back to A. Kolmogorov, "Zur Theorie der Markoffschen Ketten" (Math. Annalen 112, 1936), who showed that reversibility of a chain can be read off its transition probabilities around closed cycles. Kelly's Chapter 1 (§§1.1–1.7) states the criterion for chains (Theorem 1.7) and processes (Theorem 1.8), together with the detailed-balance characterization (Theorems 1.2, 1.3), the cut and tree lemmas (1.4, 1.5), the monotonicity of relative entropy (Theorem 1.6), truncation and rate alteration (Lemma 1.9, Corollary 1.10), and the description of the time-reversed process (Theorems 1.12–1.14). This mission is the first in a series covering the book.

Setting

Let $\mathcal S$ be a finite state space. A continuous-time Markov process $X(t)$, $t\in\mathbb R$, is specified by transition rates $q(j,k)\ge 0$, $j\ne k$, with Kelly's convention $q(j,j)=0$. Its generator is the matrix $Q$ with $Q(j,k)=q(j,k)$ off the diagonal and $Q(j,j)=-\sum_{k\ne j}q(j,k)$, and its transition matrices are $P(t)=e^{tQ}$. The rates are irreducible if every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers $\pi(j)$ summing to one that satisfy the equilibrium equations

$$\pi(j)\sum_{k}q(j,k)=\sum_k\pi(k)q(k,j),\qquad j\in\mathcal S. \qquad (1.3)$$

The stationary process with rates $q$ and equilibrium distribution $\pi$ has finite-dimensional distributions

$$P\bigl(X(t_1)=j_1,\dots,X(t_n)=j_n\bigr)=\pi(j_1)\prod_{r=1}^{n-1}P(t_{r+1}-t_r)(j_r,j_{r+1}),\qquad t_1\le\dots\le t_n .$$

It is reversible (Kelly, p. 5) if $(X(t_1),\dots,X(t_n))$ has the same distribution as $(X(\tau-t_1),\dots,X(\tau-t_n))$ for all $t_1,\dots,t_n,\tau$. The rates satisfy detailed balance with $\pi$ if $\pi(j)q(j,k)=\pi(k)q(k,j)$ for all $j,k$, and Kolmogorov's cycle condition if

$$q(j_1,j_2)q(j_2,j_3)\cdots q(j_{n-1},j_n)q(j_n,j_1)=q(j_1,j_n)q(j_n,j_{n-1})\cdots q(j_3,j_2)q(j_2,j_1)\qquad (1.22)$$

for every finite sequence of states $j_1,\dots,j_n$. The discrete-time analogue replaces rates by a stochastic matrix $p(j,k)$ and $P(t)$ by the matrix power $P^t$, $t\in\mathbb Z_{\ge 0}$.

Formalization targets

Goal: Theorem 1.8 (p. 23)

For a stationary, irreducible Markov process on a finite state space,

$$X\ \text{is reversible}\iff q\ \text{satisfies (1.22) for every finite sequence of states}.$$

The left side is a statement about the joint laws of the process at all finite sets of times; the right side involves the rates alone, not even the equilibrium distribution.

Milestones

1. Theorems 1.2 and 1.3: reversibility of a stationary chain or process is equivalent to the existence of a positive, normalized solution of detailed balance, and that solution is the equilibrium distribution.
2. Theorem 1.7: Kolmogorov's criterion (1.21) for chains. (The platform's proved rate-level equivalence of (1.22) with detailed balance under two-way communication, Serfozo's Theorem 2.8, is included as a reference item but is not a milestone: it is not Kelly's statement.)
3. Lemmas 1.4 and 1.5: the flux across any cut balances, and a process whose graph is a tree is reversible.
4. Theorem 1.6: $H(t)=\sum_j\pi(j)h(u_j(t)/\pi(j))$ is strictly increasing for $t>0$ when $h$ is strictly concave and the initial distribution is not the equilibrium one.
5. Lemma 1.9 and Corollary 1.10: altering the rates across a cut by a factor $c>0$, or truncating to a subset, preserves reversibility with explicit equilibrium distributions.
6. Theorems 1.12–1.14: the reversed process $X(\tau-t)$ is stationary Markov with rates $q'(j,k)=\pi(k)q(k,j)/\pi(j)$; conditions (1.27)–(1.28) identify it; and dynamic reversibility is characterized by $\pi(j)=\pi(j^+)$ and $\pi(j)q(j,k)=\pi(k^+)q(k^+,j^+)$.

Significance

Theorem 1.8 is the working test for reversibility throughout the book and the queueing literature: a model's reversibility, and with it a product-form equilibrium obtained by solving detailed balance, can be decided by checking a finite list of cycles in its transition diagram. Theorem 1.3 converts the distributional property into equations that later chapters solve explicitly; Theorems 1.12 and 1.13 underlie the treatment of quasi-reversible queues and networks in Chapter 3; Lemma 1.9 and Corollary 1.10 produce the equilibria of loss systems and queues with shared buffers.

The algebraic content of several of these results is already proved on the platform at the level of rates: detailed balance implies the equilibrium equations, the reversed rates preserve $\pi$, truncation preserves detailed balance, and Kolmogorov's criterion is equivalent to detailed balance for two-way communicating rates. What is not formalized anywhere is the process-level statement: that these conditions are equivalent to the time-reversal symmetry of the finite-dimensional distributions built from $e^{tQ}$. This mission supplies that layer, which connects the rate identities to the probabilistic notion they are meant to capture.

Difficulty

The rate-level identities are short; the difficulty is the passage between them and the process. Reversibility constrains the joint law at every finite set of times, and that law is built from the matrix exponential $e^{tQ}$, whose entries are not explicit functions of the rates. Relating the two requires the analytic facts about $e^{tQ}$ for a generator (stationarity of $\pi$, the semigroup property, behaviour as $t\to 0$, strict positivity of the entries for $t>0$ under irreducibility) that Mathlib does not yet provide for Markov generators, together with bookkeeping for tuples of times given in arbitrary order, with ties. For Theorem 1.8 a positive, normalized equilibrium has to be produced from the cycle condition alone, on rates that may vanish in one direction only: two-way communication is not a hypothesis, so the platform's proved rate-level criterion does not apply directly. A first attempt that defines reversibility as detailed balance avoids all of this and proves nothing new; it is excluded below.

Formalization scope

The state space is a Fintype with decidable equality; Kelly allows a countable state space, and this restriction is stated in every item. Rates are q : S → S → ℝ with 0 ≤ q j k for j ≠ k and q j j = 0 as hypotheses. The transition matrices are NormedSpace.exp (t • generator q). Time sets are ℝ (processes) and ℤ (chains). Finite-dimensional distributions are defined for arbitrary finite tuples of time points by sorting them with Tuple.sort. Equilibrium means positive, summing to one, and satisfying (1.3) (resp. $\pi P=\pi$), and every theorem takes the equilibrium distribution of the stationary process as a hypothesis. Existing platform definitions are reused: FullBalance, DetailedBalance and reversedRates from KellyStochasticNetworks_Balance, the stochastic-matrix vocabulary of mm_basic, and truncatedRates from KellyStochasticNetworks_LossNetwork.

Reversibility is not defined as detailed balance or as equality of $q$ with its reversed rates: under such a definition Theorems 1.2 and 1.3 would be tautologies and Theorem 1.8 would be the already proved rate-level criterion. It is the distributional definition of p. 5. Kolmogorov's condition ranges over all sequences of all lengths, repetitions allowed, and two-way communication is not assumed.

A complete development needs the matrix exponential of a generator (positivity, the semigroup property, the derivative at $0$, and $\pi e^{tQ}=\pi$), which is reusable for any finite-state continuous-time Markov chain, and a lemma on reversing sorted tuples. Lemma 1.1 (a general stationary process) and Lemma 1.11 (a non-stationary reversal) are not included. Proofs of any milestone, and generalizations to countable state spaces, are welcome.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 1. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• A. Kolmogorov, "Zur Theorie der Markoffschen Ketten", Mathematische Annalen 112 (1936), 155–160. https://doi.org/10.1007/BF01565412
• R. Serfozo, Introduction to Stochastic Networks, Springer, 1999, Chapter 1. https://doi.org/10.1007/978-1-4612-1482-3
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 1. https://doi.org/10.1017/CBO9781139565363

Motivation

For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp $\tfrac12 n\log n$ location and window $n$, in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.

Setting

A family of chains is a sequence $P^{(n)}$ on state spaces $V_n$ with stationary distributions $\pi_n$; all single-chain quantities acquire an index $n$. As before, $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$, $d_n(t)=\max_x\|P^{(n)t}(x,\cdot)-\pi_n\|_{TV}$, $t^{(n)}_{\mathrm{mix}}(\varepsilon)=\min\{t:d_n(t)\le\varepsilon\}$, and $t^{(n)}_{\mathrm{mix}}=t^{(n)}_{\mathrm{mix}}(1/4)$. The family has a cutoff when for every $0<\varepsilon<1$

$$\frac{t^{(n)}_{\mathrm{mix}}(\varepsilon)}{t^{(n)}_{\mathrm{mix}}(1-\varepsilon)}\;\longrightarrow\;1\qquad(n\to\infty),$$

and a cutoff at $t_n$ with window $w_n$ when $w_n=o(t_n)$ and the distance at time $t_n+\alpha w_n$ tends (in the appropriate limsup/liminf sense) to $1$ as $\alpha\to-\infty$ and to $0$ as $\alpha\to+\infty$. The separation distance from $x$ is $s_x(t)=\max_y\bigl(1-P^t(x,y)/\pi(y)\bigr)$ (Mission III), $s(t)=\max_xs_x(t)$, and a separation cutoff is defined by the same window template with $s$ in place of $d$. From Mission VII, $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ is the relaxation time; from Mission VI, $t_{\mathrm{hit}}=\max_{x,y}\mathbb E_x(\tau_y)$ and $t_{\mathrm{cov}}$ are the maximal hitting and cover times, and the pairwise distance $\bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{TV}$ is from Mission II.

The concrete chains: the lazy biased walk on $\{0,\dots,n\}$ holds with probability $\tfrac12$ and otherwise steps up with probability $p>\tfrac12$, down with probability $1-p$ (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on $\{0,1\}^n$. The lamplighter chain $G^\ast$ over a graph $G$ has states (lamp configuration in $\{0,1\}^{V}$, lamplighter position in $V$); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on $G$, and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.

Formalization targets

Goal

Theorem 18.3: the lazy hypercube walk has a cutoff at $\tfrac12\,n\log n$ with window $n$ — the family's total variation distance undergoes its full collapse in a window of size $\Theta(n)$ around $\tfrac12 n\log n$.

Milestones

• Lemma 18.1 — cutoff is equivalent to the step-function limit: $d_n(\lfloor c\,t^{(n)}_{\mathrm{mix}}\rfloor)\to1$ for every $c<1$ and $\to0$ for every $c>1$.
• Theorem 18.2 — the lazy biased walk on $\{0,\dots,n\}$ with bias $\beta=p-\tfrac12>0$ has a cutoff at $\beta^{-1}n$ with window $\sqrt n$.
• Proposition 18.4 (the product condition) — for a reversible family with $t^{(n)}_{\mathrm{mix}}\to\infty$, if $t^{(n)}_{\mathrm{mix}}\le C\,t^{(n)}_{\mathrm{rel}}$ for a fixed constant $C$, the family has no cutoff: $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ is necessary.
• Theorem 18.8 — the lazy hypercube walk has a separation cutoff at $n\log n$ with window $n$ — at twice the total-variation cutoff time.
• Lemma 19.3 (Aldous–Diaconis) — the separation–total-variation relation $s(2t)\le1-\bigl(1-\bar d(t)\bigr)^2$ for reversible chains.
• Theorem 19.1 — for lamplighter chains over a growing family of connected graphs, $t_{\mathrm{rel}}(G_n^\ast)\asymp t_{\mathrm{hit}}(G_n)$: the relaxation time is comparable, with universal constants, to the maximal hitting time of the base walk.
• Theorem 19.2 — likewise $t_{\mathrm{mix}}(G_n^\ast)\asymp t_{\mathrm{cov}}(G_n)$: the lamplighter's mixing time is governed by the base walk's cover time.

Significance

The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the $\tfrac12 n\log n$ location with window $n$ is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.

Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.

Difficulty

The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ($\lambda_j=1-j/n$ with multiplicity $\binom nj$, via Mission VII's spectral representation) and the $\ell^2$ bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time $\tfrac12 n\log n+\alpha n$). Proposition 18.4 converts an eigenfunction with eigenvalue near $1$ into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over $n$, limits in the window parameter $\alpha$) exercises the filter library in earnest.

Formalization scope

Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over $n$ composed with limits in the real parameter $\alpha$ (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants $c_1,c_2$ and the threshold $N$ are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times $t$.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• D. Aldous, P. Diaconis, Shuffling cards and stopping times, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821
• P. Diaconis, The cutoff phenomenon in finite Markov chains, Proc. Natl. Acad. Sci. USA 93 (1996). https://doi.org/10.1073/pnas.93.4.1659
• Y. Peres, D. Revelle, Mixing times for random walks on finite lamplighter groups, Electron. J. Probab. 9 (2004). https://doi.org/10.1214/EJP.v9-198

Motivation

Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$; $\|\mu-\nu\|_{TV}=\max_{A}|\mu(A)-\nu(A)|$, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ as in the earlier missions; $\pi_{\min}=\min_x\pi(x)$. The chain is lazy when $P(x,x)\ge\tfrac12$ at every state.

A martingale adapted to the chain is a family $M_t$ of functions of the trajectory up to time $t$ such that the conditional expectation of $M_{t+1}$, given the trajectory so far, equals $M_t$ — for a finite chain, a pointwise finite-sum identity. A stopping time $\tau$ is a $\{0,1\}$-valued stopping rule in the sense of Mission III: whether to stop at time $t$ depends only on the trajectory up to $t$.

From Mission IV: the edge measure is $Q(x,y)=\pi(x)P(x,y)$, with $Q(S,y)=\sum_{x\in S}Q(x,y)$, and the bottleneck constant $\Phi_\star$ is the minimum over sets $S$ with $0<\pi(S)\le\tfrac12$ of $\Phi(S)=Q(S,S^c)/\pi(S)$. The evolving-set process is the Markov chain on subsets of $V$ in which, from the current set $S$, one draws $u$ uniform on $(0,1]$ and passes to the superlevel set

$$S'=\Bigl\{y\;:\;\frac{Q(S,y)}{\pi(y)}\ge u\Bigr\}$$

— states currently receiving a large share of the flow out of $S$ are likely to join, states receiving little are likely to leave.

Formalization targets

Goal

Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —

$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\frac{2}{\Phi_\star^{2}}\,\log\!\Bigl(\frac{1}{\varepsilon\,\pi_{\min}}\Bigr).$$

Milestones

• Corollary 17.7, the Optional Stopping Theorem — if $M$ is a martingale adapted to the chain, bounded uniformly by a constant, and $\tau$ is an almost surely finite stopping time, then $\mathbb E_x(M_\tau)=M_0(x)$: stopping a fair game at a fair time wins nothing.
• Lemma 17.12 — the evolving-set process, started from the singleton $\{x\}$, recovers the chain: $P^t(x,y)=\dfrac{\pi(y)}{\pi(x)}\,\mathbb P_{\{x\}}\{y\in S_t\}$.
• Lemma 17.13 — for the evolving-set process, the stationary mass $\pi(S_t)$ of the current set is a martingale.
• Theorem 17.17 — return probabilities of the lazy random walk on a graph of maximum degree $\Delta$: $\bigl|P^t(x,x)-\pi(x)\bigr|\le\sqrt2\,\Delta^{5/2}/\sqrt t$, an application of the evolving-set machinery.

Significance

The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound $t_{\mathrm{mix}}\lesssim\Phi_\star^{-2}\log(1/\pi_{\min})$ of Mission VII, but it needs no reversibility, and its proof technique — controlling the root $\sqrt{\pi(S_t)}$ as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.

Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.

Difficulty

The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series $\sum_t\mathbb P\{\tau=t\}\,M_t$ must be shown summable and equal to $M_0$ by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from $S$ to $T$ is the length of the set of $u\in(0,1]$ whose superlevel set is exactly $T$, which the formalization encodes by explicit upper and lower thresholds (a min over $T$ and a max over $T^c$ of the clipped ratios $Q(S,y)/\pi(y)$); establishing that these lengths sum to one over $T$, and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on $\sqrt{\pi(S_t)}$: laziness keeps the thresholds in $[\tfrac12,1]$, an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of $\mathbb E\sqrt{\pi(S_t)\bigl(1-\pi(S_t)\bigr)}$, and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.

Formalization scope

Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by $\prod P(\omega_i,\omega_{i+1})$, with expectations over the stopping time as tsums in $t$ (non-summable families sum to $0$; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to $1$). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume $\pi$ positive and $P$ lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with $\pi(x)=\deg(x)/2|E|$ written out. Real-valued bounds on the natural-valued $t_{\mathrm{mix}}$ are direct inequalities on the cast, with no hidden rounding.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• B. Morris, Y. Peres, Evolving sets, mixing and heat kernel bounds, Probab. Theory Related Fields 133 (2005). https://doi.org/10.1007/s00440-005-0434-7
• D. Williams, Probability with Martingales, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9780511813658

Motivation

The Ising model is statistical mechanics' fruit fly: spins $\pm1$ on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature $\beta$ — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small $\beta$) the dynamics mixes in $O(n\log n)$ steps on any bounded-degree graph; on the complete graph the same dynamics passes, as $\beta$ crosses an explicit threshold, from $O(n\log n)$ mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.

Setting

Spin configurations on a finite graph $G$ with vertex set of size $n$ and maximum degree $\Delta$ are functions $\sigma$ assigning $\pm1$ to each vertex (encoded over Booleans, $\mathrm{true}\mapsto+1$). The Ising model at inverse temperature $\beta>0$ is the Gibbs distribution

$$\pi(\sigma)\;=\;\frac{e^{\,\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)}}{Z(\beta)},$$

each edge counted once, $Z(\beta)$ the normalizing partition function. The Glauber dynamics for $\pi$ picks a uniform vertex and re-samples its spin from $\pi$ conditioned on all other spins — concretely, the new spin at $v$ is $+1$ with probability $\bigl(1+\tanh(\beta S)\bigr)/2$ where $S$ is the sum of the neighbouring spins.

The yardsticks are as in the earlier missions: $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance, $d(t)=\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$. From Mission VII: an eigenvalue of a chain is a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$; $\lambda_2$ is the largest eigenvalue $\ne1$, the spectral gap is $\gamma=1-\lambda_2$, $\lambda_\star$ the largest $|\lambda|$ over eigenvalues $\ne1$, and the relaxation time is $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$.

Formalization targets

Goal

Theorem 15.1, the high-temperature fast-mixing theorem: if $\Delta\tanh\beta<1$ then the Glauber dynamics on any graph satisfies

$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{n\,\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\Delta\tanh\beta}\Bigr\rceil,$$

together with its refinement for graphs with all degrees even, where the condition relaxes to $(\Delta/2)\tanh(2\beta)<1$.

Milestones

• Lemma 15.2 (the tanh lemma) — the elementary inequalities about $x\mapsto\tanh(\beta(x+1))-\tanh(\beta(x-1))$ (symmetry, monotonicity, the bounds by $2\tanh\beta$ and, at odd integers, by $\tanh 2\beta$) that drive the one-site coupling contraction.
• Theorem 15.3 — the dynamical phase transition on the complete graph at $\beta=\alpha/n$: (i) for $\alpha<1$, $t_{\mathrm{mix}}(\varepsilon)\le n(\log n+\log(1/\varepsilon))/(1-\alpha)$; (ii) for $\alpha>1$, there are $r(\alpha),C>0$ with $t_{\mathrm{mix}}\ge C\,e^{r n}$ — split here into a fast half and a slow half.
• Theorem 15.4 — on the $n$-cycle, at every $\beta>0$, mixing is $n\log n$ up to explicit constants: $(1+o(1))\,\frac{n\log n}{2c_O(\beta)}\le t_{\mathrm{mix}}(\varepsilon)\le(1+o(1))\,\frac{n\log n}{c_O(\beta)}$ with $c_O(\beta)=1-\tanh(2\beta)$.
• Theorem 15.6 (Kenyon–Mossel–Peres) — on the rooted $b$-ary tree of depth $k$ with $n_k$ vertices, the relaxation time is polynomial at every temperature: $t_{\mathrm{rel}}\le n_k^{\,c_T(\beta,b)}$ with $c_T(\beta,b)=2\beta(3b+1)/\log b+1$.
• Proposition 15.7 — removing $r$ edges changes the spectral gap of the Glauber dynamics by at most a factor $e^{2\beta(\Delta+2r)}$.
• Theorem 15.9 — the block-dynamics comparison: if blocks $V_1,\dots,V_b$ cover the vertex set, each of size at most $M$, each vertex in at most $M_\star$ blocks, then the spectral gap $\gamma_B$ of the block dynamics and the gap $\gamma$ of the single-site dynamics satisfy $\gamma_B\le M^2M_\star\,(4e^{2\beta\Delta})^{M+1}\,\gamma$.

Significance

The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.

Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their $\tanh$ closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.

Difficulty

The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate $1-\bigl(1-\Delta\tanh\beta\bigr)/n$, and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space $\{\pm1\}^V$ has size $2^n$, so all "polynomial" bounds are polynomial in $n$, not in the size of the state space.

Formalization scope

The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the $\tanh$ closed form is a provable lemma, not a definition. Asymptotic statements ($o(1)$, "for sufficiently large $n$") are rendered with explicit $\exists N,\forall n\ge N$ quantifiers and a free precision parameter $\delta$; the phase-transition constants $r(\alpha),C$ are existentially quantified. The tree is encoded as words of length $\le k$ over an alphabet of size $b$; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• C. Kenyon, E. Mossel, Y. Peres, Glauber dynamics on trees and hyperbolic graphs, FOCS 2001. https://doi.org/10.1109/SFCS.2001.959934
• D. A. Levin, M. J. Luczak, Y. Peres, Glauber dynamics for the mean-field Ising model: cut-off, critical power law, and metastability, Probab. Theory Related Fields 146 (2010). https://doi.org/10.1007/s00440-008-0189-z
• F. Martinelli, Lectures on Glauber dynamics for discrete spin models, Lectures on Probability Theory and Statistics (Saint-Flour XXVII), Springer, 1999. https://doi.org/10.1007/978-3-540-48115-7_2

Motivation

How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the $L$-reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").

Setting

All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position $0$ on top. Random transpositions have increment distribution $\mu(\mathrm{id})=1/n$, $\mu(\text{transposition})=2/n^2$. The lazy adjacent-transposition walk puts mass $1/2$ on the identity and $1/[2(n-1)]$ on each $(i\ i{+}1)$. One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled $0$ to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The $L$-reversal chain on circular arrangements indexed by $\mathbb Z_n$ picks a position $i$ and a length $k<L$ uniformly and reverses the segment $[i,i+k]$.

Formalization targets

Goal

$$t_{\mathrm{mix}}\;\le\;(2+o(1))\,n\log n$$

for random transpositions on $n$ cards (Corollary 8.10), formalized as: for every $\delta>0$ there is $N$ with $t_{\mathrm{mix}}\le(2+\delta)n\log n$ for all $n\ge N$.

Milestones

Proposition 8.11 (random transpositions lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\frac{n-1}{2}\log\bigl(\frac{(1-\varepsilon)n}{6}\bigr)$, via fixed points); Proposition 8.13 (riffle shuffle: $t_{\mathrm{mix}}\le 2\log_2(4n/3)+1$); Proposition 8.14 (riffle shuffle: $t_{\mathrm{mix}}(\varepsilon)\ge(1-\delta)\log_2 n$ for large $n$, by the counting bound of Mission IV); the random adjacent transpositions upper bound $t_{\mathrm{mix}}(\varepsilon)\le 2n^3\log_2 n$ for large $n$ (§16.1.2, display (16.4)) and lower bound $t_{\mathrm{mix}}\ge n^2(n-1)/16$ (§16.1.3, by following a single card); and Proposition 16.2 (the $L$-reversal chain with $L<n/2$ satisfies $d\bigl((1-\varepsilon)\frac n2\log n\bigr)\to1$, via conserved adjacencies).

Significance

The results. Random transpositions at $\frac12 n \log n$ (the constant $2$ here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at $\frac32\log_2 n$ are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for $n=52$. The adjacent-transposition walk at order $n^3\log n$ is the basic example where geometry (diameter $\binom n2$) forces polynomial mixing. The $L$-reversal lower bound is the quantitative starting point of the biological application.

Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.

Difficulty

Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra $\log n$ factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after $t$ transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after $t$ inverse shuffles the deck is a uniform stable sort of $t$-bit labels, and mixing reduces to the birthday problem for $2^t$ labels; formalizing "distinct labels imply uniform order" is the crux. The $L$-reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.

Formalization scope

All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular $L$-reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements ($o(1)$, "for sufficiently large $n$") are spelled out with explicit $\forall\delta\,\exists N$ quantifiers; upper bounds carry a $+1$ where integer rounding requires it. The $L$-reversal family takes the length function $L(n)$ as a hypothesis-carrying parameter with $1\le L(n)<n/2$, and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to $1$).

Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• P. Diaconis, M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981). https://doi.org/10.1007/BF00535487
• D. Bayer, P. Diaconis, Trailing the dovetail shuffle to its lair, Ann. Appl. Probab. 2 (1992). https://doi.org/10.1214/aoap/1177005705
• R. Durrett, Shuffling chromosomes, J. Theoret. Probab. 16 (2003). https://doi.org/10.1023/A:1024940217006

Why abandonment matters in call centers

Telephone call centers are among the largest employers of service labour, and their staffing decisions are made with queueing models. The classical model is the Erlang-C queue $M/M/N$: Poisson arrivals, $N$ agents, exponential service, infinitely patient callers. Real callers hang up. Garnett, Mandelbaum and Reiman (M&SOM 2002) argued that a model ignoring abandonment is misleading exactly in the regime where large call centers operate, near full utilization: the Erlang-C queue is unstable when the offered load exceeds the number of agents, while a real center simply loses the excess callers. They advocated the Erlang-A queue $M/M/N+M$, in which each caller also has an exponential patience, and developed its many-server asymptotics.

The first of their asymptotic results, Theorem 1 of the paper, settles the most basic performance measure, the fraction of callers who abandon, to first order as the center grows. Its proof combines a utilization argument with two monotonicity properties proved by Bhattacharya and Ephremides (1991) and an asymptotic expansion of Erlang's loss formula due to Jagerman (1974).

The Erlang-A queue

Callers arrive as a Poisson process of rate $\lambda>0$. There are $N\ge1$ statistically identical agents, each serving one caller at a time with exponentially distributed service times of rate $\mu>0$. The waiting room is unlimited and is served in order of arrival. Each caller carries a patience, an exponential random variable of rate $\theta>0$ independent of everything else; a caller whose wait in queue reaches his patience abandons and does not return.

The number of callers in the system, $Q$, is a birth–death process with birth rate $\lambda$ in every state and death rate

$$\mu_k=\min(k,N)\,\mu+(k-N)^+\,\theta$$

in state $k$. Its stationary distribution (Appendix B of the paper, with infinite buffer) is

$$\pi_k=\frac{(\lambda/\mu)^k}{k!}\,\pi_0\ (0\le k\le N),\qquad \pi_k=\prod_{j=N+1}^{k}\frac{\lambda}{N\mu+(j-N)\theta}\cdot\frac{(\lambda/\mu)^N}{N!}\,\pi_0\ (k>N),$$

with $\pi_0$ normalizing. The abandonment probability $P_N\{Ab\}$ is the probability that a caller arriving in steady state abandons. An arrival finding $N+n$ callers in the system abandons with probability $(n+1)\theta/(N\mu+(n+1)\theta)$, so

$$P_N\{Ab\}=\sum_{n\ge0}\pi_{N+n}\,\frac{(n+1)\theta}{N\mu+(n+1)\theta}.$$

The blocking probability $P_N\{Bl\}$ of the loss system $M/M/N/N$ with the same rates is Erlang's formula $E(\lambda/\mu,N)=\dfrac{(\lambda/\mu)^N/N!}{\sum_{j=0}^{N}(\lambda/\mu)^j/j!}$.

The asymptotic regime. The $N$-th system has $N$ agents, arrival rate $\lambda_N$, service rate $\mu$ independent of $N$, and patience rate $\theta_N$. As in §4 of the paper, $\lambda_N\to\infty$ and $\theta_N\to\theta\in(0,\infty)$. The traffic intensity is $\rho_N=\lambda_N/(N\mu)$.

Formalization targets

Goal: Theorem 1 (p. 215)

If $\rho_N\to\rho_\infty$ for some $0\le\rho_\infty\le\infty$, then

$$\lim_{N\to\infty}P_N\{Ab\}=\begin{cases}0,&0\le\rho_\infty\le1,\\ 1-1/\rho_\infty,&\rho_\infty>1,\end{cases}$$

with $1-1/\infty=1$. The limit does not depend on $\theta$.

Milestones

1. The explicit $\pi$ is the unique steady state of the Erlang-A birth–death process (Appendix B).
2. Equation (2): $\theta\,E[\#\text{ waiting}]=\lambda P\{Ab\}$.
3. Utilization below one: $\lambda_N(1-P_N\{Ab\})<N\mu$.
4. Property (ii): $P_N\{Ab\}$ is increasing in $\theta$.
5. $P_N\{Ab\}\to P_N\{Bl\}$ as $\theta\to\infty$.
6. $P_N\{Ab\}\le P_N\{Bl\}$ for every $0<\theta<\infty$.
7. Erlang's formula is increasing in the offered load (published and proved: KellyStochasticNetworks.erlang_strictMono).
8. Jagerman's expansion (10) of $P_N\{Bl\}$ for $\lambda_N=N\mu\rho_\infty$, $\rho_\infty>1$, as an asymptotic equivalence.
9. If $\lambda_N=N\mu\rho_\infty+o(N)$ with $\rho_\infty>1$, then $P_N\{Bl\}\to1-1/\rho_\infty$ and $\limsup_N P_N\{Ab\}\le 1-1/\rho_\infty$.
10. Property (i): $P_N\{Ab\}$ is increasing in $\lambda$.

Significance

Theorem 1 is the law-of-large-numbers description of an overloaded or critically loaded many-server queue with abandonment. It says that an overloaded center sheds exactly its excess load, $\lambda_N-N\mu$, to abandonment, and that a critically loaded center ($\rho_\infty=1$) already has vanishing abandonment. This is what directs attention to the Halfin–Whitt (quality-and-efficiency-driven) regime $\sqrt N(1-\rho_N)\to\beta$, where the paper's later results (Theorems 2 and 4) refine the picture to order $1/\sqrt N$. It is also the fluid-scale input of later work on staffing with abandonment.

The theorem has been proved in the paper; to our knowledge none of the statements above has a machine-checked proof. The mission produces a formal model of the Erlang-A queue with its stationary law, a verified bridge between the Erlang-A and Erlang-B (loss) systems, and a formal limit theorem for Erlang's loss formula under linear load, each reusable in other many-server problems.

Difficulty

The heuristic is immediate: utilization is at most one, so $\lambda_N(1-P_N\{Ab\})\le N\mu$ gives the lower bound $1-1/\rho_N$. The upper bound is the substance. A direct estimate of the series defining $P_N\{Ab\}$ involves $\theta$-dependent products whose asymptotics are not elementary, and the result must hold uniformly over patience rates $\theta_N$ that are only known to be positive. Two further obstacles remain: the monotonicity of $P_N\{Ab\}$ in $\theta$ and in $\lambda$ is a stochastic-ordering property of the birth–death process, not a term-by-term inequality between the series, and any comparison with the loss system needs the asymptotics of Erlang's formula under a load that is linear in $N$ only up to $o(N)$. Nothing is assumed about how $\rho_N$ approaches its limit, so the critical case $\rho_\infty=1$ cannot be read off from either side.

Formalization scope

• Model. All objects live in the namespace ErlangA.Abandonment. The death rates, the unnormalized weights $w_k$, $\pi_k=w_k/\sum_j w_j$ (a tsum) and $P_N\{Ab\}$ are explicit definitions of the parameters $N\in\mathbb N$ and $\lambda,\mu,\theta\in\mathbb R$; $P_N\{Bl\}$ is the published KellyStochasticNetworks.erlang (λ/μ) N.
• Steady state. "Stationary" means a probability distribution on $\{0,1,2,\dots\}$ solving the global balance equations (the published QueueingFundamentals.BirthDeath.IsSteadyState). The time limit $\lim_t P\{Q(t)=n\}$ is not formalized. The buffer is infinite.
• Abandonment probability. $P_N\{Ab\}$ is defined by the arrival-sees-time-average form above; the balance form $(\theta/\lambda)\sum_k(k-N)^+\pi_k$ is milestone 2. It is a probability per arriving caller, not the abandonment rate and not the probability that someone is waiting.
• Sequences. $N$ is both the index and the number of agents; hypotheses on the $N$-th system are imposed for $N\ge1$. $\mu>0$ is fixed.
• Limits. $\rho_\infty\in[0,\infty]$ is an extended nonnegative real and $\rho_N\to\rho_\infty$ is convergence in $[0,\infty]$; $1-1/\rho_\infty$ is evaluated there, giving $1$ at $\rho_\infty=\infty$. All limits are Filter.Tendsto along $N\to\infty$; "$\sim$" is Asymptotics.IsEquivalent; $\limsup\le c$ is "for every $\varepsilon>0$, eventually $\le c+\varepsilon$".
• Monotonicity. "Increasing" in properties (i) and (ii) is read as nondecreasing, in one parameter at a time with the others fixed.
• Ruling out trivial readings. Because $\pi$ is a quotient by a tsum, a divergent normalizing series would make $\pi\equiv0$ and $P_N\{Ab\}=0$, which would make the underloaded case of the goal vacuous; milestone 1 asserts that $\pi$ is a genuine probability distribution for every $N\ge1$ and $\lambda,\mu,\theta>0$, and the goal is stated for exactly these parameters.
• Welcome contributions. Stochastic-ordering arguments for birth–death processes (for properties (i) and (ii)), asymptotics of Erlang's loss formula (Jagerman's expansion, or a direct proof of the linear-load limit), and summation identities for the stationary law.

Selected references

• O. Garnett, A. Mandelbaum, M. Reiman, Designing a Call Center with Impatient Customers, Manufacturing & Service Operations Management 4(3):208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
• P. P. Bhattacharya, A. Ephremides, Stochastic monotonicity properties of multiserver queues with impatient customers, Journal of Applied Probability 28(3):673–682, 1991. https://doi.org/10.2307/3214500
• D. L. Jagerman, Some properties of the Erlang loss function, Bell System Technical Journal 53(3):525–551, 1974. https://doi.org/10.1002/j.1538-7305.1974.tb02756.x
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice $\mathbb Z^d$ is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."

Setting

Continuous time (Ch. 20). For a finite chain $P$, the heat kernel at time $t\ge0$ is defined by Poissonization,

$$H_t(x,y)=\sum_{k=0}^{\infty}e^{-t}\frac{t^k}{k!}\,P^k(x,y),$$

the law at time $t$ of a walk taking $P$-steps at Poisson arrival times ($=e^{t(P-I)}$ as a matrix exponential). With $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$, the continuous distance and mixing time are $d^{\mathrm{cont}}(t)=\max_x\|H_t(x,\cdot)-\pi\|_{TV}$ and $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)=\inf\{t\ge0:d^{\mathrm{cont}}(t)\le\varepsilon\}$. The lazy version of a discrete chain is $\tfrac12(I+P)$; from Mission VII, the spectral gap $\gamma$ is $1-\lambda_2$ with $\lambda_2$ the largest eigenvalue $\ne1$. The product chain on a product of $n$ coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.

Countable state spaces (Ch. 21). A chain on a countable state space $V$ is a function $P$ with nonnegative entries and rows summing to one (as convergent series); $t$-step probabilities $P^t(x,y)$ are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to $x$ is $\tau_x^+=\min\{t\ge1:X_t=x\}$; a state is recurrent when $\mathbb P_x\{\tau_x^+<\infty\}=1$ (tails tend to zero), positive recurrent when moreover $\mathbb E_x(\tau_x^+)<\infty$ (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative $\pi$ summing to one with $\pi P=\pi$ (as convergent series). Simple random walk on $\mathbb Z^d$ steps from $x$ to one of its $2d$ nearest neighbours uniformly at random.

Formalization targets

Goal

Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:

1. for $d\le2$, simple random walk on $\mathbb Z^d$ is recurrent — it returns to its starting point with probability one;
2. for $d\ge3$, it is transient — with positive probability it never returns.

Milestones

• Theorem 20.1 — for any irreducible finite chain, aperiodic or not, the heat kernel converges: $d^{\mathrm{cont}}(t)\to0$ as $t\to\infty$.
• Theorem 20.3 — the two-way comparison between lazy discrete and continuous mixing: eventual $\varepsilon$-mixing of the lazy chain at time $k$ gives $2\varepsilon$-mixing of the heat kernel at time $k$, and $\varepsilon$-mixing of the heat kernel at time $m$ gives $2\varepsilon$-mixing of the lazy chain at time $4m$.
• Theorem 20.6 — the spectral bound for reversible chains: $\bigl|H_t(x,y)-\pi(y)\bigr|\le\sqrt{\pi(y)/\pi(x)}\;e^{-\gamma t}$.
• Theorem 20.7 — mixing of continuous-time product chains: with all coordinate gaps $\ge\gamma$ and coordinate stationary masses bounded below, $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)\le(2\gamma)^{-1}n\log n+\gamma^{-1}n\log(1/(c_0\varepsilon))$, with a matching $\tfrac{n}{2\gamma}\log n$ lower bound when the gaps are equal — the $n\log n$ product-chain phenomenon.
• Proposition 21.3 — the recurrence dichotomy on countable spaces: a state is recurrent exactly when its Green's function $\sum_tP^t(x,x)$ diverges, and for an irreducible chain one recurrent state makes all states recurrent.
• Theorem 21.12 — an irreducible countable chain is positive recurrent if and only if it has a stationary distribution.
• Lemma 21.13 (Kac) — for an irreducible chain with stationary distribution $\pi$ and any nonempty set $S$: $\sum_{x\in S}\pi(x)\,\mathbb E_x(\tau_S^+)=1$; in particular $\mathbb E_x(\tau_x^+)=1/\pi(x)$.
• Theorem 21.14 — the convergence theorem on countable spaces: an irreducible, aperiodic, positive recurrent chain has a unique stationary distribution $\pi$, and $\|P^t(x,\cdot)-\pi\|_{TV}\to0$ from every start.
• Theorem 21.17 — in the null recurrent case, $P^t(x,y)\to0$ for all pairs of states: no stationary profile is approached.

Significance

The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the $n\log n$ paradigm (independent coordinates mix in relaxation time $\times\log(\text{number of coordinates})$) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension-$d$ paradigm.

Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the $d\ge3$ half has never been formalized in any assistant to our knowledge.

Difficulty

The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because $H_t(x,x)>0$ for $t>0$. The product-chain bounds need the $\ell^2$ machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity $G(x,x)=1/\mathbb P_x\{\tau_x^+=\infty\}$ handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities ($P^{2t}(0,0)\asymp t^{-d/2}$, obtained by Stirling in $d=1,2$ and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.

Formalization scope

Chapter 20 lives on finite state spaces: the heat kernel is a tsum over $k$ of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk $0$ if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds ($\exists K,\forall k\ge K$), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, $t$-step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of $\mathbb Z^d$ with the walk defined by nearest-neighbour steps; the $d\le2$ and $d\ge3$ halves are separate conjuncts of one statement.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• G. Pólya, Über eine Aufgabe der Wahrscheinlichkeitsrechnung betreffend die Irrfahrt im Straßennetz, Math. Ann. 84 (1921). https://doi.org/10.1007/BF01458701
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002. https://www.stat.berkeley.edu/~aldous/RWG/book.html