Markov Chains and Mixing Times XI: The Cutoff Phenomenon and Lamplighter WalksTextbook
## 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
18 thms6 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times X: Martingales and Evolving SetsTextbook
## 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 `Finset`s, 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 `tsum`s 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
12 thms6 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times IX: The Ising ModelTextbook
## 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
17 thms6 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times V: Shuffling CardsTextbook
## 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
19 thms6 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times XII: Continuous Time and Countable State SpacesTextbook
## 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
17 thms5 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times IV: Lower Bounds on Mixing TimesTextbook
## Motivation
Missions II–III produce upper bounds on mixing times. Whether such a bound is *sharp* is a different question: an $O(n^2)$ bound on a chain that actually mixes in $n\log n$ steps hides the truth. Chapter 7 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009) develops the standard toolkit of lower bounds: the counting and diameter bounds (a chain cannot spread faster than its transition graph allows), the **bottleneck ratio** (a chain cannot mix faster than it crosses its worst cut), and **distinguishing statistics** (a chain is far from stationarity as long as some statistic separates $P^t(x,\cdot)$ from $\pi$ by several standard deviations). The bottleneck bound — closely related to the conductance of the chain and, via Mission VII, to the Cheeger inequality — is the single most important obstruction result in the subject: it is how slow mixing (torpid mixing of Ising at low temperature, in Mission IX) is proved.
## Setting
For a chain $P$ with stationary distribution $\pi$, the **edge measure** is $Q(x,y)=\pi(x)P(x,y)$, the **bottleneck ratio** of a set $S$ of states is
$$\Phi(S)=\frac{Q(S,S^{c})}{\pi(S)},\qquad Q(S,S^c)=\sum_{x\in S,\,y\notin S}\pi(x)P(x,y),$$
and the bottleneck ratio of the chain is $\Phi_\star=\min\{\Phi(S):\pi(S)\le\tfrac12,\ S\neq\varnothing\}$. The maximal one-step out-degree is $\Delta=\max_x|\{y:P(x,y)>0\}|$; the diameter is measured in the graph joining $x\ne y$ when $P(x,y)+P(y,x)>0$. For a statistic $f:V\to\mathbb R$ and distribution $\mu$, $\mathbb E_\mu(f)$ and $\operatorname{Var}_\mu(f)$ are the finite-sum expectation and variance, and $\mu f^{-1}$ denotes the pushforward of $\mu$ under $f$.
## Formalization targets
### Goal
$$t_{\mathrm{mix}}\;\ge\;\frac{1}{4\Phi_\star}.$$
This is Theorem 7.3, the bottleneck-ratio lower bound, the chapter's central theorem.
### Milestones
The counting bound $t_{\mathrm{mix}}(\varepsilon)\ge\log\bigl(|V|(1-\varepsilon)\bigr)/\log\Delta$ for chains with uniform stationary distribution (§7.1.1, display (7.2)); the diameter bound: any two states satisfy $\mathrm{dist}(x_0,y_0)\le 2\,t_{\mathrm{mix}}(\varepsilon)$ for $\varepsilon<1/2$ (§7.1.2, display (7.3)); Proposition 7.8 (a statistic separating means by $r$ standard deviations forces $\|\mu-\nu\|_{\mathrm{TV}}\ge1-4/(4+r^2)$); Lemma 7.9 (projection under a statistic does not increase TV distance); Proposition 7.13 (the lazy hypercube walk satisfies $d(\tfrac12 n\log n-\alpha n)\ge 1-8e^{1-2\alpha}$); and Proposition 7.14 (the top-to-random shuffle needs $n\log n-O(n)$ shuffles, matching the upper bound of Mission III).
## Significance
*The results.* Together with Mission III this pins the top-to-random shuffle at $n\log n\pm O(n)$ — the first sharp mixing result of the series, and the prototype of the cutoff phenomenon formalized in Mission XI. Proposition 7.13 similarly matches the hypercube upper bound and feeds the cutoff analysis. The bottleneck bound is used in Mission IX to prove exponentially slow mixing of the mean-field Ising model at low temperature, and its two-sided refinement is the Cheeger inequality of Mission VII.
*Formalizing them.* Mathlib has no notion of conductance/bottleneck ratio of a chain, no distinguishing-statistic method, and no mixing-time lower bound of any kind. The pushforward and variance infrastructure over finitely supported distributions is elementary but new, and reusable wherever second-moment methods appear (Wilson's method in Mission VII).
## Difficulty
The bottleneck theorem's proof is short but exact: it hinges on the identity $\pi(S)\|\mu_S P-\mu_S\|_{\mathrm{TV}}=Q(S,S^c)$ for $\pi$ conditioned on $S$, followed by a telescoping estimate of $\|\mu_S P^t-\mu_S\|_{\mathrm{TV}}$; the formal cost is manipulating conditioned measures and one-sided TV sums (Remark 4.3 from Mission II). For Proposition 7.8, the second-moment argument runs through Chebyshev on both distributions plus optimization of a threshold — the constants $4/(4+r^2)$ are exact, not asymptotic, so the formal inequalities must be done carefully. Proposition 7.13 requires the binomial mean/variance computation for Hamming weight under both $\pi$ and $P^t(\mathbf 1,\cdot)$, including the negative-correlation bound for unrefreshed coordinates. The naive route to a lower bound — "the chain has not left a small set, so it is far from $\pi$" — is precisely the counting bound and is too weak for the sharp results; the statistics method is what closes the gap.
## Formalization scope
$\Phi_\star$ is an infimum over the subtype of nonempty sets with $\pi(S)\le\tfrac12$; on a one-point space this subtype is empty and the infimum takes a junk value, making the goal trivially true there (the bound carries content only for $|V|\ge2$, as in the book). The counting bound divides by $\log\Delta$ with total division ($\Delta\le1$ gives a trivially true statement). The diameter bound is stated for arbitrary pairs of states through `SimpleGraph.dist` of the transition graph, which subsumes the book's diameter formulation. Propositions 7.13 and 7.14 are stated for all integer times $t\le\frac12 n\log n-\alpha n$ (resp. $t\le n\log n-\alpha n$), using monotonicity of $d$ instead of evaluating at a real-valued time — this avoids floor artifacts while keeping the book's content. Proposition 7.14 quantifies "$\alpha$ large, then $n$ large" exactly as the book's iterated limit.
Welcome contributions: monotonicity of $d(t)$ in $t$; conditioned-measure lemmas; variance API for `distExp`/`distVar`.
## 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
- M. Jerrum, A. Sinclair, *Approximating the permanent*, SIAM J. Comput. 18 (1989). https://doi.org/10.1137/0218077
- D. Aldous, P. Diaconis, *Shuffling cards and stopping times*, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821
12 thms5 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times III: Coupling and Strong Stationary TimesTextbook
## Motivation
The Convergence Theorem of Mission II says an irreducible aperiodic chain mixes geometrically, but with constants coming from a crude Doeblin decomposition — useless for actual chains, whose state spaces are exponentially large. Chapters 5–6 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009) develop the two classic probabilistic techniques that give *useful* upper bounds: **coupling** — run two copies of the chain jointly so that they meet quickly, and read a TV bound off the meeting time — and **strong stationary times** — random times at which the chain is *exactly* stationary, independent of the time. The flagship application is the top-to-random shuffle: repeatedly take the top card of a deck of $n$ cards and reinsert it at a uniform position; the deck is well mixed after $n\log n + cn$ shuffles, with error at most $e^{-c}$.
## Setting
A **Markovian coupling** of a chain $P$ (with the stay-together convention (5.2)) is a chain $Q$ on pairs whose coordinate marginals are both $P$ and which moves diagonal states to diagonal states. The **coupling time** $\tau_{\mathrm{couple}}$ is the hitting time of the diagonal; its tails are expressed with the trajectory calculus of Mission I.
A **randomized stopping time** is presented by its stopping rule: for each time $t$ and trajectory prefix $\omega$, a number $s_t(\omega)\in[0,1]$, the conditional probability of stopping at $t$ given the trajectory so far and no earlier stop. A **strong stationary time** for the chain started at $x$ is an almost surely finite such $\tau$ with
$$\mathbb P_x\{\tau=t,\ X_\tau=y\}=\mathbb P_x\{\tau=t\}\,\pi(y),$$
i.e. $X_\tau\sim\pi$ independent of $\tau$. The **separation distance** is $s_x(t)=\max_y\,[1-P^t(x,y)/\pi(y)]$.
The mission also fixes the concrete chains it bounds: the lazy walk on the discrete torus $\mathbb Z_n^d$, the Metropolis chain on proper $q$-colorings of a graph, the Glauber dynamics of the hardcore model with fugacity $\lambda$, and the top-to-random shuffle on decks of $n$ cards (states are arrangements, i.e. permutations; position $0$ is the top).
## Formalization targets
### Goal
Let $d(t)= \max_x\|P^t (x,\cdot)−\pi\|_{TV}$,
$$d\bigl(\lceil n\log n+\alpha n\rceil\bigr)\;\le\;e^{-\alpha}\qquad(\alpha>0)$$
for the top-to-random shuffle on $n\ge2$ cards — display (6.16) of the book, the chapter's flagship bound, proved by combining the strong stationary time $\tau_{\mathrm{top}}$ with the coupon collector tail of Mission I.
### Milestones
Theorem 5.2 and Corollary 5.3 (the coupling bound: $\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}}\le\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$, hence $d(t)\le\max_{x,y}\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$); Theorem 5.5 ($t_{\mathrm{mix}}(\varepsilon)\le c(d)\,n^2\log_2\varepsilon^{-1}$ for the lazy torus walk); Theorem 5.7 (Metropolis colorings, $q>3\Delta$: mixing in $O(n\log n)$); Theorem 5.8 (hardcore Glauber, $\lambda<(\Delta-1)^{-1}$: mixing in $O(n\log n)$); Proposition 6.1 with Example 6.7 ($\tau_{\mathrm{top}}$ is a strong stationary time); Lemma 6.11 ($s_x(t)\le\mathbb P_x\{\tau>t\}$); Lemma 6.13 ($\|P^t(x,\cdot)-\pi\|_{\mathrm{TV}}\le s_x(t)$); Proposition 6.10 ($d(t)\le\max_x\mathbb P_x\{\tau>t\}$).
## Significance
*The results.* The coupling bound is the single most used upper-bound technique in the subject: Missions VIII (path coupling), IX (Ising) and XI (cutoff examples) all instantiate it. Strong stationary times and separation distance return in Mission XI (separation cutoff) and underlie perfect sampling in Mission XIII. The three concrete bounds (torus, colorings, hardcore) are the standard first applications and give the first polynomial mixing results of the series; the colorings and hardcore chains are the objects of intense ongoing research on sampling thresholds.
*Formalizing them.* Nothing here exists in Mathlib. The novel infrastructure is the stopping-rule formalization of randomized stopping times over trajectory prefixes — measure-theory-free, but expressive enough for the strong stationarity identity — and the Markovian-coupling predicate on pair chains. Both are reused later in the series (Matthews method, cutoff, CFTP).
## Difficulty
The coupling bound itself is short once Proposition 4.7 (Mission II) is available; the work is in the applications. For the torus, the coordinatewise coupling requires assembling $d$ one-dimensional couplings and bounding the coupling time by a sum of one-dimensional meeting times — the formal bookkeeping of "couple coordinate by coordinate" is the real cost, and the constant $c(d)$ absorbs it. For Theorem 5.7 and 5.8 the argument is a grand coupling over all colorings/configurations simultaneously; the formal statements quantify only over the resulting bound, but a solver must build the coupling. For Proposition 6.1, the crux is the induction "given $k$ cards under the original bottom card, all $k!$ orders are equally likely" — an exchangeability argument that must be carried through the stopping-rule encoding. Lemma 6.11 is where the definition of strong stationarity does its work; the naive attempt to prove Proposition 6.10 directly from the coupling characterization fails, which is exactly why separation distance is introduced.
## Formalization scope
Couplings of chains are transition matrices on $V\times V$ with marginal conditions stated row by row; the stay-together convention is part of the predicate, matching (5.2). Stopping rules take the trajectory prefix (which includes the starting state), so times "depending on the starting position" are covered; strong stationarity packages the stopping rule bounds, almost-sure finiteness ($\sum_t\mathbb P_x\{\tau=t\}=1$), and the product identity. The colorings chain lives on the subtype of proper colorings; the hardcore chain is the Glauber dynamics of Mission II restricted to the subtype of hardcore configurations (transitions never leave it). Mixing-time upper bounds carry an explicit $+1$ for integer rounding where the book's real-valued display would otherwise be false for the integer-valued $t_{\mathrm{mix}}$. The torus statement fixes $\varepsilon\le 1/2$; for $\varepsilon$ near $1$ the display is false as stated in the book.
Welcome contributions: interface lemmas between `setAvoidTailProb` of the pair chain and the two coordinates; the taboo-matrix form of coupling-time tails; exchangeability infrastructure for the deck chains (reused in Mission V).
## 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, J. A. Fill, *Strong stationary times via a new form of duality*, Ann. Probab. 18 (1990). https://doi.org/10.1214/aop/1176990628
22 thms5 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook
## Motivation
The coupling method of Mission III asks for a coupling of two copies of a chain from *every* pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009) replaces that global demand by a local one. The **path coupling** technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across *edges*; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the **transportation metric** (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for *counting* colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.
## Setting
All chains live on a finite state space $V$ with a transition matrix $P$; $P^t(x,\cdot)$ is the time-$t$ distribution from $x$, $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A **coupling** of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$.
Given a metric-like cost $\rho$ on pairs of states, the **transportation metric** between two distributions is the cheapest expected cost of moving one onto the other:
$$\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.$$
Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$, the **path metric** $\rho(x,y)$ is the least total length of a $G$-path from $x$ to $y$.
For the colorings application: a $q$-coloring of the vertices of a graph is **proper** when adjacent vertices receive distinct colors, and the **Glauber dynamics** on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.
## Formalization targets
### Goal
Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$-colorings, if $q>2\Delta$ then
$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.$$
### Milestones
- **Lemma 14.3 and Remark 14.2** — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
- **Theorem 14.6, path coupling** (Bubley–Dyer) — if for every *edge* $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$.
- **Corollary 14.7** — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$, where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
- **Theorem 14.12, approximate counting** — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$-colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.
## Significance
*The results.* Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$-hard counting problems.
*Formalizing them.* Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.
## Difficulty
The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires *gluing* two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.
## Formalization scope
The transportation metric is an `sInf` over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an `sInf` over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$" is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.
## 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
- R. Bubley, M. Dyer, *Path coupling: a technique for proving rapid mixing in Markov chains*, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
- M. Jerrum, *A very simple algorithm for estimating the number of k-colorings of a low-degree graph*, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
- M. Jerrum, L. Valiant, V. Vazirani, *Random generation of combinatorial structures from a uniform distribution*, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X
9 thms4 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times VII: Eigenvalues and the Cheeger InequalityTextbook
## Motivation
How fast does a Markov chain forget its starting point? For a *reversible* chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always $1$, and the size of the gap between $1$ and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009) develop this spectral theory and culminate in the discrete **Cheeger inequality** of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap $\gamma$ (an analytic quantity, defined below) and the bottleneck constant $\Phi_\star$ (a geometric quantity from Mission IV, also recalled below) control each other:
$$\frac{\Phi_\star^2}{2}\;\le\;\gamma\;\le\;2\,\Phi_\star.$$
A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.
## Setting
All chains live on a finite state space $V$. A chain with transition matrix $P$ and stationary distribution $\pi$ is **reversible** when the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the **total variation distance** $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$, the worst-case distance to stationarity $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$, and the **mixing time** $t_{\mathrm{mix}}(\varepsilon)=\min\{t: d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$; we write $\pi_{\min}=\min_x\pi(x)$.
The spectral vocabulary: an **eigenfunction** of $P$ is a nonzero $f:V\to\mathbb R$ with $Pf=\lambda f$, where $(Pf)(x)=\sum_yP(x,y)f(y)$; the number $\lambda$ is then an **eigenvalue**. Out of the spectrum one forms
- $\lambda_2$, the largest eigenvalue different from $1$, and the **spectral gap** $\gamma=1-\lambda_2$;
- $\lambda_\star$, the largest *absolute value* of an eigenvalue different from $1$, the **absolute gap** $\gamma_\star=1-\lambda_\star$, and the **relaxation time** $t_{\mathrm{rel}}=1/\gamma_\star$.
Functions on $V$ carry the weighted inner product $\langle f,g\rangle_\pi=\sum_xf(x)g(x)\pi(x)$ — the geometry, denoted $\ell^2(\pi)$, in which a reversible $P$ is self-adjoint — and the **Dirichlet form**
$$\mathcal E(f)=\tfrac12\sum_{x,y}\bigl[f(x)-f(y)\bigr]^2\,\pi(x)P(x,y),$$
the average squared variation of $f$ along the chain's transitions. Finally, from Mission IV: the **bottleneck ratio** of a set $S$ of states is $\Phi(S)=\sum_{x\in S,\,y\notin S}\pi(x)P(x,y)\,/\,\pi(S)$, the conditional probability at stationarity of escaping $S$ in one step, and the **bottleneck constant** is $\Phi_\star=\min\{\Phi(S):\varnothing\ne S,\ \pi(S)\le\tfrac12\}$.
## Formalization targets
### Goal
Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,
$$\frac{\Phi_\star^2}{2}\;\le\;\gamma\;\le\;2\,\Phi_\star.$$
### Milestones
- **Lemma 12.1** — every eigenvalue satisfies $|\lambda|\le1$; for an irreducible chain the eigenfunctions of the eigenvalue $1$ are the constant functions; an irreducible aperiodic chain does not have $-1$ as an eigenvalue.
- **Lemma 12.2** — the spectral representation: a reversible chain admits eigenfunctions $f_1,\dots,f_{|V|}$, orthonormal with respect to $\langle\cdot,\cdot\rangle_\pi$, with eigenvalues $\lambda_j$, such that $P^t(x,y)/\pi(y)=\sum_jf_j(x)f_j(y)\lambda_j^t$ for all $t,x,y$.
- **Theorem 12.3** — mixing is at most relaxation times a log factor: $t_{\mathrm{mix}}(\varepsilon)\le\log\bigl(1/(\varepsilon\,\pi_{\min})\bigr)\,t_{\mathrm{rel}}+1$.
- **Theorem 12.4** — mixing is at least the relaxation time: $t_{\mathrm{mix}}(\varepsilon)\ge(t_{\mathrm{rel}}-1)\log\bigl(1/(2\varepsilon)\bigr)$.
- **§12.3.1** — the model computation: simple random walk on the $n$-cycle has the numbers $\cos(2\pi j/n)$, $j=0,\dots,n-1$, among its eigenvalues.
- **Theorem 13.1** — if every pair of states admits a coupling of the two one-step distributions that contracts some metric $\rho$ on $V$ by a factor $\theta$ in expectation, then $\lambda_\star\le\theta$.
- **Theorem 13.5, Wilson's method** — an eigenfunction $\Phi$ with eigenvalue $\lambda\in(\tfrac12,1)$ whose one-step increments have second moment at most $R$ yields the explicit lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\bigl[2\log(1/\lambda)\bigr]^{-1}\bigl[\log\bigl((1-\lambda)\Phi(x)^2/(2R)\bigr)+\log\bigl((1-\varepsilon)/\varepsilon\bigr)\bigr]$.
- **Lemmas 13.11–13.12** — the variational characterization: $\gamma$ is the minimum of $\mathcal E(f)$ over functions with mean zero ($\sum_xf(x)\pi(x)=0$) and unit norm ($\langle f,f\rangle_\pi=1$), and the minimum is attained.
- **Lemma 13.22** — the comparison method: if a second reversible chain $\tilde P$ on the same space, with stationary distribution $\tilde\pi$, Dirichlet form $\tilde{\mathcal E}$, and gap $\tilde\gamma$, satisfies $\tilde{\mathcal E}(f)\le B\,\mathcal E(f)$ for every $f$, then $\tilde\gamma\le\bigl[\max_x\pi(x)/\tilde\pi(x)\bigr]B\,\gamma$.
## Significance
*The results.* Theorems 12.3–12.4 sandwich the mixing time between $t_{\mathrm{rel}}$ and $t_{\mathrm{rel}}\log(1/\pi_{\min})$ — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).
*Formalizing them.* Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.
## Difficulty
Everything routes through one change of basis: conjugating $P$ by the diagonal matrix with entries $\sqrt{\pi(x)}$ produces a matrix that is *symmetric* precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to $\ell^2(\pi)$, keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of $\lambda_2$ and $\lambda_\star$ as suprema over the set of non-unit eigenvalues (finite, and nonempty once $|V|\ge2$) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set $S$, recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal $f$, decomposes it over its level sets $\{f>c\}$, and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.
## Formalization scope
Eigenvalues are defined by real eigenvectors ($\exists f\ne0,\ Pf=\lambda f$); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. $\lambda_2$ and $\lambda_\star$ are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis $|V|\ge2$, matching the book's implicit assumption of a non-degenerate chain. $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ with total inverse. Theorem 12.3 carries an explicit $+1$ absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.
Welcome contributions: the symmetrization API (conjugation by $\mathrm{diag}(\sqrt{\pi})$), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.
## 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
- M. Jerrum, A. Sinclair, *Approximating the permanent*, SIAM J. Comput. 18 (1989). https://doi.org/10.1137/0218077
- G. F. Lawler, A. D. Sokal, *Bounds on the L² spectrum for Markov chains and Markov processes*, Trans. Amer. Math. Soc. 309 (1988). https://doi.org/10.1090/S0002-9947-1988-0930082-9
- D. B. Wilson, *Mixing times of lozenge tiling and card shuffling Markov chains*, Ann. Appl. Probab. 14 (2004). https://doi.org/10.1214/aoap/1042765669
24 thms4 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook
## Motivation
A reversible Markov chain *is* an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009) develop the dictionary and its two crown results: the **commute time identity** of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$, and the **Matthews method** bounding cover times by hitting times with harmonic-number precision.
## Setting
A **network** is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities $$P(x,y)=c(x,y)/c(x)$$ where $c(x)=\sum_y c(x,y)$, and $c_G=\sum_x c(x)$. A function $h$ is **harmonic** at $x$ if $h(x)=\sum_y P(x,y)h(y)$. The **voltage** with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$, the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$, and the **effective resistance** is $R(a\leftrightarrow z)=\|I\|^{-1}$. A **flow** from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$. Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$, their expectations, the Green's function $G_{\tau_z}(a,x)$, the maximal hitting time $t_{\mathrm{hit}}$, and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.
## Formalization targets
### Goal
$$\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).$$
This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.
### Milestones
Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$); Proposition 11.4 (the matching Matthews lower bound over subsets).
## Significance
*The results.* The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.
*Formalizing them.* Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.
## Difficulty
The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.
## Formalization scope
Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is *defined* probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.
Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.
## 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. G. Doyle, J. L. Snell, *Random Walks and Electric Networks*, MAA, 1984. https://arxiv.org/abs/math/0001057
- A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, *The electrical resistance of a graph captures its commute and cover times*, STOC 1989. https://doi.org/10.1145/73007.73062
- P. Matthews, *Covering problems for Markov chains*, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894
15 thms4 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook
# Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution
## Motivation
Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one **stationary distribution** — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$. Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$, so nothing in the subject can be formalized before this mission is.
This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, *Markov Chains and Mixing Times* (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$). Later missions in the series build on the definitions published here.
## Setting
A chain on a finite state space $\Omega$ is presented by its **transition matrix**, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$. A **distribution** is a row vector $\mu$ with nonnegative entries summing to $1$; one step of the chain carries $\mu$ to $\mu P$, and the $t$-step transition probabilities are the entries of the matrix power $P^t$.
The chain is **irreducible** if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$. The **period** of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$, and the chain is **aperiodic** if every state has period $1$. A distribution $\pi$ is **stationary** if $\pi P = \pi$, and $\pi$ and $P$ are in **detailed balance** (the chain is *reversible*) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$.
Trajectory events over a finite horizon are finite sums of path weights: a length-$t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$, with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$, and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$, formalized as a `tsum` over $t$.
## Formalization targets
### Goal
$$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$$
This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.
### Milestones toward and around the goal
The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with
$$\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$$
(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).
## Significance
*The result itself.* Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.
*Formalizing it.* Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (`mm_basic`, `mm_path`, `mm_classical`) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.
## Difficulty
The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$, or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging `tsum` with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.
## Formalization scope
States form a `Fintype` with decidable equality; chains are `Matrix V V ℝ` with the row-stochasticity predicate `IsStochastic`; distributions are functions `V → ℝ` with the predicate `IsDist`. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$, which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are `tsum`s of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$) so that junk values cannot make them vacuously true. Existence statements carry a `Nonempty V` hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws `Fin t → Fin n`, uniform sign strings `Fin r → Bool`), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.
Contributions welcome beyond the milestone list: `simp` lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting `pathWeight` sums to matrix powers — these will be reused by every later mission in the series.
## 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
- J. R. Norris, *Markov Chains*, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
- D. Aldous, J. A. Fill, *Reversible Markov Chains and Random Walks on Graphs*, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html
20 thms4 active usersReviewed
🏆Completed
Captain: tianyipeng
Markov Entanglement: Index Policies for Restless Bandits are Asymptotically SeparableResearch Paper
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.
12 thms2 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times XIII: Coupling from the PastTextbook
## 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
5 thms2 active usersReviewed
🏆Completed
Captain: Shuze Chen
Markov Chains and Mixing Times II: The Convergence TheoremTextbook
## 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).