Markov Chain

Motivation

A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of $J$ stations costs $J$ one-dimensional calculations instead of one exponentially large one.

Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as $\lambda_{jk}\varphi_j(n_j)$: a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and $s$-server queues, infinite-server queues, and networks of them, open or closed.

Setting

There are $J$ colonies, and a state is a vector $n = (n_1,\dots,n_J)$ of non-negative integers, $n_j$ being the number of individuals in colony $j$. Three operators move one individual:

$$T^{jk}n \ \text{ moves one from } j \text{ to } k, \qquad T^{j\to}n \ \text{ removes one from } j, \qquad T^{\to k}n \ \text{ adds one to } k .$$

An open migration process is the Markov process on $\mathbb{Z}_+^J$ with transition rates

$$q(n, T^{jk}n)=\lambda_{jk}\varphi_j(n_j), \qquad q(n, T^{j\to}n)=\mu_j\varphi_j(n_j), \qquad q(n, T^{\to k}n)=\nu_k ,$$

where $\varphi_j(0)=0$: nothing leaves an empty colony. Immigration into colony $k$ is Poisson of rate $\nu_k$. Taking $\mu\equiv 0$ and $\nu\equiv 0$ and restricting to states of a fixed total $\sum_j n_j = N$ gives a closed migration process. Setting $\varphi_j(n)=\min(n,s)$ models an $s$-server queue at colony $j$; $\varphi_j(n)=n$ models individuals moving independently.

The traffic equations define $(\alpha_j)$ from the rates. In the open case they are

$$\alpha_j\Bigl(\mu_j+\sum_k \lambda_{jk}\Bigr) \;=\; \nu_j+\sum_k \alpha_k\lambda_{kj}, \qquad j = 1,\dots,J,$$

and in the closed case $\alpha_j\sum_k \lambda_{jk}=\sum_k \alpha_k\lambda_{kj}$ with $\alpha_j>0$ and $\sum_j\alpha_j=1$. Finally set

$$g_j=\sum_{n=0}^{\infty}\frac{\alpha_j^{\,n}}{\prod_{r=1}^{n}\varphi_j(r)} .$$

Formalization targets

Goal — Theorem 2.8, the product form of an open migration process

If $g_1,\dots,g_J<\infty$ then

$$\pi(n)=\prod_{j=1}^{J}\pi_j(n_j), \qquad \pi_j(m)=g_j^{-1}\,\frac{\alpha_j^{\,m}}{\prod_{r=1}^{m}\varphi_j(r)}$$

is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over $\mathbb{Z}_+^J$. Both halves are asserted, because the first alone is satisfied by every positive multiple of $\pi$ and the second is what makes the convergence hypothesis $g_j<\infty$ do work.

Supporting levels

The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates $\lambda'_{jk}=\alpha_k\lambda_{kj}/\alpha_j$, $\mu'_j=\nu_j/\alpha_j$ and $\nu'_k=\alpha_k\mu_k$; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.

Significance

The result itself. Theorem 2.8 says that at a fixed time the occupancies $n_1,\dots,n_J$ of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate $\alpha_j\lambda_j$ — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.

Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) — and none of it is open. What the mission produces is a machine-checked model of a queueing network: the migration operators, the rate matrix, the traffic equations and the product form, in a form later missions in this series import rather than restate. Mathlib has no queueing theory and no theory of continuous-time Markov chains on a countable state space, so this is the first such development. It builds on the DetailedBalance / FullBalance layer published in mission I.

Difficulty

An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony $j$ (rate of individuals leaving colony $j$ equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.

The formal obstacle is different and worth naming. The equilibrium equation at a state $n$ sums over the states that can jump into $n$, and the naive transcription $\sum_{j,k}\pi(T^{jk}n)q(T^{jk}n,n)$ silently assumes $T^{jk}n$ is a state, which fails when $n_j=0$. Over $\mathbb{Z}_+^J$ such a term must be dropped, and a formalization that keeps it — with $n_j-1$ read as truncated subtraction — states something false.

Formalization scope

The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy counts, with J finite; no irreducibility is assumed, since none of the statements below need it. Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a sum of indicator terms over the possible transitions, so the equilibrium equations can be stated as the FullBalance predicate of mission I, with unconditional sums over the countable state space. This is what avoids the trap above: a sum over actual states never includes a would-be-negative one, and any spurious coincidence of operators at a boundary carries a $\varphi_j(0)=0$ factor and contributes nothing.

Conventions the development commits to: $\lambda_{jj}=0$, so a transfer is always between distinct colonies; $\varphi_j(0)=0$ and $\varphi_j(r)>0$ for $r\ge 1$; $\alpha_j>0$; and $g_j$ is asserted via HasSum, which states convergence and the value at once, rather than as an extended real that might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and reversed-rate statements carry an explicit $n_j\ge 1$ where the book's state space carries it implicitly; the goal itself does not need such a guard.

A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by $\pi\equiv 0$, whereas the requirement that $\pi$ sum to $1$ forces the constants $g_j$ to be exactly the ones stated.

Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 2 (pp. 22–48); Theorems 2.4, 2.8, 2.9, 2.13, equations (2.1)–(2.6). DOI 10.1017/cbo9781139565363
• James R. Jackson, Networks of waiting lines, Operations Research 5 (1957), 518–521. DOI 10.1287/opre.5.4.518
• P. Whittle, Equilibrium distributions for an open migration process, Journal of Applied Probability 5 (1968), 567–571. DOI 10.2307/3211921
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapters 2 and 3.
• David G. Kendall, Some problems in mathematical genealogy, in Perspectives in Probability and Statistics (J. Gani, ed.), Academic Press, 1975, 325–345.
• John D. C. Little, A proof for the queuing formula: $L = \lambda W$, Operations Research 9 (1961), 383–387. DOI 10.1287/opre.9.3.383

Motivation

In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.

The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.

Setting

A link carries $C$ parallel circuits. Calls arrive as a Poisson process of rate $\lambda$ and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter $\mu$; holding times are independent of one another and of the arrival times. A call that arrives to find all $C$ circuits busy is lost — it does not queue.

Let $X(t)\in\{0,1,\dots,C\}$ be the number of busy circuits. Then $X$ is a Markov process with transition rates

$$q(j,j+1)=\lambda \quad (j=0,\dots,C-1), \qquad q(j,j-1)=j\mu \quad (j=1,\dots,C),$$

and $q(j,k)=0$ otherwise. A collection of numbers $\pi=(\pi(j))$ is in detailed balance with rates $q$ when

$$\pi(j)\,q(j,k)=\pi(k)\,q(k,j)\qquad\text{for all }j,k,$$

and satisfies the equilibrium (full balance) equations when

$$\pi(j)\sum_k q(j,k)=\sum_k \pi(k)\,q(k,j)\qquad\text{for all }j .$$

Detailed balance is the statement that, in equilibrium, transitions from $j$ to $k$ occur as frequently as transitions from $k$ to $j$. Writing $\nu=\lambda/\mu$ for the traffic intensity, Erlang's formula is

$$E(\nu,C)=\frac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}.$$

Formalization targets

Goal — Erlang's formula

$$\pi \text{ in detailed balance with } q, \ \sum_{j=0}^{C}\pi(j)=1 \quad\Longrightarrow\quad \pi(C)=E\!\left(\tfrac{\lambda}{\mu},C\right).$$

The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly $E(\nu,C)$ to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.

Supporting levels

$$\pi(j)=\frac{\nu^{j}}{j!}\,\pi(0), \qquad \sum_{j=0}^{C} j\,\pi(j)=\nu\bigl(1-E(\nu,C)\bigr), \qquad \frac{d}{d\nu}E(\nu,C)=-\bigl(1-E(\nu,C)\bigr)\bigl(E(\nu,C)-E(\nu,C-1)\bigr),$$

together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates $q'(j,k)=\pi(k)q(k,j)/\pi(j)$ and retains $\pi$ as an equilibrium distribution, and $q'=q$ holds exactly when $\pi$ and $q$ are in detailed balance.

Significance

The result itself. $E(\nu,C)$ is the blocking probability of the link, so it converts a traffic measurement $\nu$ and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean $1/\mu$, which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes $E(\nu,C)$ tractable in optimization: it shows $E$ is increasing in $\nu$, and the recursion it encodes is how the formula is evaluated numerically without overflow.

Formalizing it. Nothing here is open mathematics; the value of the mission is a machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no theory of detailed balance or of reversible Markov processes over a countable state space, so this mission contributes the first: the predicates DetailedBalance and FullBalance, the reversed rate matrix, and the three structural facts relating them. Those are shared by every later mission in this series — the migration processes of Chapter 2 and the loss networks of Chapter 3 are all proved reversible or quasi-reversible by exactly these means.

Difficulty

The obvious route to $\pi(C)$ is to solve the equilibrium equations directly, and for a birth-and-death chain that is a three-term recursion whose general solution needs two boundary conditions. Detailed balance replaces it with a two-term recursion and one boundary condition, and the whole content of the reversibility section is that the substitution is legitimate. The remaining work is bookkeeping that Lean makes less forgiving than the page does: the detailed balance equations must be indexed so that the $j=0$ and $j=C$ boundaries are not silently assumed away, the normalizing sum must be shown positive before it can be inverted, and the induction that produces $\nu^{j}/j!$ has to carry the Fin (C+1) index through Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives $\left(\sum_{j\le C-1}\nu^{j}/j!\right)$ in the numerator, and recognizing it as $\bigl(1-E(\nu,C)\bigr)$ times the denominator is the step that produces the stated form.

Formalization scope

The state space is Fin (C + 1), so the link with $C$ circuits has $C+1$ states and finiteness is built in; $\pi$ is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a PMF, so that the normalization $\sum_j \pi(j) = 1$ appears explicitly wherever it is used. FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the same predicate serves the countable chains of later chapters; over a Fintype it is the finite sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that a Markov process must change state when it jumps.

The rates carry $\lambda,\mu>0$ as hypotheses. This rules out the degenerate reading in which $\mu = 0$ makes every downward rate vanish: with $\mu=0$ the detailed balance equations force $\pi(j)\lambda = 0$ for $j<C$, so the only normalized solution is the point mass at $C$, and $\pi(C)=1$ while Lean evaluates $E(\lambda/0,C)=E(0,C)=0$ for $C\ge1$; the goal would be false. Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so it cannot be satisfied by a degenerate reindexing.

Contributions welcome beyond the listed items: the insensitivity of $E(\nu,C)$ to the holding time distribution, the recursion $E(\nu,C)=\nu E(\nu,C-1)/(C+\nu E(\nu,C-1))$, the finite-source variant $\pi_M(j)\propto\binom{M}{j}(\eta/\mu)^{j}$ and the PASTA statement that an arriving call in that model sees $\pi_{M-1}$, and the parking-space identity $\sum_{C\ge 0}E(\nu,C)$ of Exercise 1.9.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 1 (pp. 13–21), equations (1.2), (1.4), (1.5), Proposition 1.1, Exercises 1.7 and 1.8. DOI 10.1017/cbo9781139565363
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektrotkeknikeren 13 (1917), 5–13.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1.
• J. R. Norris, Markov Chains, Cambridge University Press, 1998. DOI 10.1017/CBO9780511810633

Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on index policies — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by value decomposition: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.

Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its measure of Markov entanglement, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.

The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its configuration: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.

The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.

Motivation

Every sampling guarantee in this series so far is approximate: run the chain for $t_{\mathrm{mix}}(\varepsilon)$ steps and the output is within $\varepsilon$ of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample exactly from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but from the past. Their algorithm, coupling from the past (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times $-1,-2,-3,\dots$; as soon as the composed map from some time $-t$ collapses the entire state space to a single value, that value is an exact sample from $\pi$. Chapter 22 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$. A random mapping representation of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:

$$\nu\{f: f(x)=y\}\;=\;P(x,y)\qquad\text{for all }x,y.$$

Sampling $f\sim\nu$ and applying it to the current state is exactly one $P$-step — simultaneously from every possible current state.

CFTP draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ indexed by past times and composes them forward from the past up to time zero:

$$F^0_{-t}\;=\;f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}.$$

Note the order: extending the horizon deeper into the past prepends new randomness inside the composition, while the maps near time $0$ stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has coalesced when $F^0_{-t}$ is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the monotone variant, $V$ carries a partial order with a bottom state $\hat0$ and a top state $\hat1$ and every update map is monotone; then it suffices to track the two extreme trajectories.

Formalization targets

Goal

Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if $\nu$ is a random mapping representation of $P$, $\pi$ is stationary for $P$, and coalescence is almost sure, then for every state $y$ the probability that the CFTP composition has coalesced to the value $y$ within $t$ steps from the past tends, as $t\to\infty$, to exactly $\pi(y)$ — the output of the algorithm is an exact sample from the stationary distribution, with no mixing-time error term.

Milestones

• Proposition 1.5 / §22.3 — every finite Markov chain has a random mapping representation: a suitable $\nu$ always exists.
• Coalescence (§22.3) — if some finite composition of update maps collapses the state space with positive probability, then coalescence is almost sure: the probability that $F^0_{-t}$ is not yet constant tends to $0$ as $t\to\infty$.
• Monotone CFTP (§22.2) — if the state space has a bottom $\hat0$ and a top $\hat1$ and every update map is monotone, then the composition is constant as soon as it merely identifies $\hat0$ and $\hat1$: checking two trajectories certifies coalescence of all of them.

Significance

The results. CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is exactly $\pi$, side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the $2^n$ trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.

Formalizing it. The correctness argument is short but famously slippery — the standard pitfall (running the coupling into the future yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.

Difficulty

The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon $t$ is the finite product of $t$ copies of $\nu$ (tuples of update maps, weighted by products); the key observation — for fixed $t$, the law of $F^0_{-t}$ applied to any fixed start equals the law of $t$ forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time $t$, the output equals $F^0_{-t}(x)$ for every $x$; choosing the start according to $\pi$ shows the output law differs from $\pi$ by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by $-t$" is increasing in $t$ because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.

Formalization scope

Update-map distributions are functions $(V\to V)\to\mathbb R$ with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition $F^0_{-t}$ is encoded by a tuple $F:\mathrm{Fin}\,t\to(V\to V)$ with $F(i)$ the map used at time $-(i{+}1)$, folded so that the last entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of $\nu$-weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to $0$, and the goal's conclusion is a limit of real sequences (Filter.Tendsto), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with OrderBot and OrderTop and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (Chapter 22, by J. G. Propp and D. B. Wilson). https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• J. G. Propp, D. B. Wilson, Exact sampling with coupled Markov chains and applications to statistical mechanics, Random Structures Algorithms 9 (1996). https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O
• D. B. Wilson, How to couple from the past using a read-once source of randomness, Random Structures Algorithms 16 (2000). https://doi.org/10.1002/(SICI)1098-2418(200003)16:2<85::AID-RSA1>3.0.CO;2-H

Motivation

The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution $\pi$. The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009), answers the two questions that make that fact useful. First, the inverse problem of sampling: given a target distribution $\pi$ — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is $\pi$? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the convergence question: in what sense, and how fast, does an irreducible aperiodic chain approach $\pi$? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.

Setting

All chains live on a finite state space $V$ and are presented by row-stochastic matrices, with the definitions of Mission I. The total variation distance between distributions $\mu$ and $\nu$ is

$$\|\mu-\nu\|_{\mathrm{TV}} = \max_{A\subseteq V}\,|\mu(A)-\nu(A)|,$$

the maximal discrepancy over events. A coupling of $\mu$ and $\nu$ is a distribution on $V\times V$ whose marginals are $\mu$ and $\nu$. For a chain $P$ with stationary $\pi$ one sets

$$d(t)=\max_x \|P^t(x,\cdot)-\pi\|_{\mathrm{TV}},\qquad \bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}},$$

and the mixing time is $t_{\mathrm{mix}}(\varepsilon)=\min\{t : d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$.

The Metropolis chain for a target $\pi$ and a symmetric proposal chain $\Psi$ accepts a proposed move $x\to y$ with probability $1\wedge \pi(y)/\pi(x)$; a general (not necessarily symmetric) base chain is handled by the ratio $\bigl(\pi(y)\Psi(y,x)\bigr)/\bigl(\pi(x)\Psi(x,y)\bigr)\wedge 1$. The Glauber dynamics for a distribution $\pi$ on configurations $V^{\text{sites}}$ picks a uniform site and re-samples its value from $\pi$ conditioned on the rest.

Formalization targets

Goal

$\text{$P$ irreducible and aperiodic}\;\Longrightarrow\;\exists\,\alpha\in(0,1),\ C>0:\quad d(t)\le C\alpha^{t}.$

This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.

Milestones

The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half-$\ell^1$ formula (Proposition 4.2 with Remark 4.3), the supremum over $[-1,1]$-bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison $d\le\bar d\le 2d$ (Lemma 4.11) and submultiplicativity $\bar d(s+t)\le\bar d(s)\bar d(t)$ (Lemma 4.12); the standard mixing-time consequences $d(\ell\, t_{\mathrm{mix}}(\varepsilon))\le(2\varepsilon)^\ell$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil\log_2\varepsilon^{-1}\rceil\, t_{\mathrm{mix}}$ (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).

Significance

The results. The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that $t_{\mathrm{mix}}(\varepsilon)$ is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half-$\ell^1$ formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of $\bar d$ is what makes $t_{\mathrm{mix}}$ a meaningful single number.

Formalizing them. None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, $d$, $\bar d$, $t_{\mathrm{mix}}$, couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.

Difficulty

The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies $P^r(x,y)\ge\delta\pi(y)$, so $P^r=(1-\theta)\Pi+\theta Q$ with $\Pi$ the rank-one matrix of rows $\pi$, and induction gives $P^{rk}=(1-\theta^k)\Pi+\theta^kQ^k$. The formal work is matrix algebra with careful bookkeeping of the remainder chain $Q$, plus the monotonicity of $d$ needed to interpolate between multiples of $r$. For Proposition 4.7 the delicate half is constructing the optimal coupling: mass $\mu\wedge\nu$ on the diagonal and the normalized product of the positive parts off it, with the degenerate case $\mu=\nu$ handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of $\pi$ have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.

Formalization scope

Total variation distance is defined as the supremum over events, $\bigsqcup_{A}\,|\mu(A)-\nu(A)|$ over Finset V, exactly as in (4.1); the half-$\ell^1$ formula is a milestone, not the definition. The mixing time is sInf of the set $\{t : d(t)\le\varepsilon\}$ in $\mathbb N$ (junk value $0$ if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. $\lceil\log_2\varepsilon^{-1}\rceil$ via Nat.ceil of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require $\pi>0$ pointwise; this matches the book, which divides by $\pi(x)$ throughout.

Welcome contributions beyond the milestones: simp lemmas for tvDist, monotonicity of $d$ and $\bar d$ in $t$, and triangle-inequality infrastructure — all reused by Missions III–XIII.

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
• N. Metropolis, A. Rosenbluth, M. Rosenbluth, A. Teller, E. Teller, Equation of state calculations by fast computing machines, J. Chem. Phys. 21 (1953). https://doi.org/10.1063/1.1699114
• W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états, Rev. Math. Union Interbalkan. 2 (1938).