Probability

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

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

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

Why canonical paths matter

A finite Markov chain moves among states according to transition probabilities. Its second largest eigenvalue measures how slowly some variation in the starting state can disappear. Directly computing that eigenvalue is often difficult when the state space is large. A geometric bound can be more useful: choose a route between each ordered pair of states and measure how much weighted traffic the routes impose on each transition. Diaconis and Stroock present this route-based bound as Proposition 7 of their 1991 paper, following the canonical-path method of Jerrum and Sinclair (Diaconis–Stroock, §3B). It makes a spectral estimate depend on the geometry of chosen routes and the stationary weight of each edge.

The paper's purpose is to compare methods for bounding eigenvalues of reversible chains. Its earlier Poincaré estimate uses weighted path lengths. Proposition 7 instead passes through a bottleneck constant and Cheeger's inequality. These are different summaries of the same chain: one examines a system of paths, and the other examines flow across every cut. The comparison is useful on graphs where paths are easy to choose but the cut minimizing the bottleneck constant is not apparent (Diaconis–Stroock, pp. 52–55).

Finite reversible chains and directed path congestion

Let $V$ be a finite state space with at least two states. A transition matrix $P$ has entries $P(x,y)\geq 0$ and each row sums to one. It is irreducible when every state can be reached from every other state in some number of steps. A stationary distribution $\pi$ is a nonnegative probability vector satisfying $\pi P=\pi$. The chain is reversible when it satisfies detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$. Write $Q(x,y)=\pi(x)P(x,y)$ for the stationary edge flow. These are the standing assumptions of the paper's §1A, restated in §3B (Diaconis–Stroock, pp. 36, 54).

For every distinct ordered pair $(x,y)$, choose a finite walk $\gamma_{xy}$ from $x$ to $y$. Every consecutive step $(u,v)$ of the walk must have $Q(u,v)>0$. The walk may revisit a vertex or an edge; §3B places no no-repetition condition on these choices. An oriented edge is an ordered pair $(u,v)$ with positive flow. A walk contains it when one of its consecutive steps traverses it in that direction. The canonical-path congestion of the chosen walk system $\Gamma$ is the paper's quantity

$$\eta(\Gamma)=\max_{e:Q(e)>0}\frac{1}{Q(e)} \sum_{x\ne y:\,e\in\gamma_{xy}}\pi(x)\pi(y).$$

The sum assigns weight $\pi(x)\pi(y)$ to an ordered pair, once for each directed edge that its chosen walk uses. Irreducibility ensures that walks between different states exist. Under the mission's assumptions the positive-flow edge set is nonempty, so the maximum has its ordinary finite meaning (Diaconis–Stroock, (3.2), p. 54).

For a nonempty set $S\subseteq V$ with $\pi(S)\leq\tfrac12$, let $Q(S\times S^{\mathrm c})$ be the total stationary flow from $S$ to its complement. The bottleneck constant is

$$h=\min_{\varnothing\ne S\subseteq V,\,\pi(S)\leq 1/2} \frac{Q(S\times S^{\mathrm c})}{\pi(S)}.$$

The denominator is positive under irreducibility. Write $\beta_1$ for the largest eigenvalue of $P$ other than the simple eigenvalue $1$, and write $\lambda_1=1-\beta_1$ for the spectral gap. These conventions match §1A and equation (3.4) (Diaconis–Stroock, pp. 36, 56).

Formalization targets

The mission's goal is Proposition 7, for every valid choice of $\Gamma$:

$$\beta_1\leq 1-\frac{1}{8\eta(\Gamma)^2}.$$

Its milestones record the source's cut argument: a selected walk from $S$ to $S^{\mathrm c}$ crosses an oriented cut edge; the total pair weight obeys $\pi(S)\pi(S^{\mathrm c})\leq\eta Q(S\times S^{\mathrm c})$; and consequently $h\geq 1/(2\eta)$. The final milestone is the already formalized version of the paper's equation (3.4), $h^2/2\leq\lambda_1\leq 2h$ (Diaconis–Stroock, pp. 54, 56).

The companion result is the graph specialization (3.3). For simple random walk on a connected graph $G=(V,E)$, let $d_*$ be the maximum degree and let $b$ be the maximum number of ordered-pair walks traversing an oriented edge. It gives

$$\beta_1\leq 1-\frac12\left(\frac{|E|}{d_*^2b}\right)^2.$$

This statement uses the exact displayed bound of Remark 3.1; the earlier sentence in that remark uses a different normalization of $\eta$ (Diaconis–Stroock, p. 55).

What the bound supplies

The proposition converts any usable path system into an explicit spectral estimate. Once a graph or chain supplies paths whose edge loads can be bounded, the formula bounds $\beta_1$ without diagonalizing $P$ or finding the set that minimizes $h$. In the graph case, equation (3.3) expresses the estimate using only the edge count, maximum degree, and maximum directed path load. The paper compares that bound with its Poincaré bound on examples including cycles, cubes, and binary trees (Diaconis–Stroock, pp. 55–56).

Equation (3.4) already has a proved formalization in the published MarkovMixing library, under the same finite reversible-chain conventions. This mission adds the paper's path-congestion definition and cut estimates, then states the still-needed Proposition 7 and graph specialization against that library. The result is a reusable connection between a chosen family of walks and a chain's existing bottleneck and spectral objects.

Where the difficulty lies

The route load $\eta$ concerns individual directed edges, whereas $h$ takes a minimum over all admissible cuts. A single heavily loaded edge does not by itself identify the minimizing cut. The central difficulty is to control, for every cut at once, all weighted ordered pairs whose walks leave it. The direction of a crossing matters: $Q(S\times S^{\mathrm c})$ counts edges directed out of $S$, and $\eta$ must count traversals of those same orientations. Omitting an orientation or allowing negative unused edge flow would invalidate the intermediate cut estimate.

There is also a printed discrepancy. Proposition 6 on p. 52 displays a stronger upper bound on $\beta_1$ than the inequality established in §3C. The mission uses equation (3.4), whose lower gap bound yields the $1/(8\eta^2)$ constant actually stated in Proposition 7 (Diaconis–Stroock, pp. 52, 54, 56).

Formalization scope

Lean represents the state space as a finite type, the chain as a real matrix, and the stationary distribution as a real function. It imports the published MarkovMixing definitions of stochasticity, irreducibility, stationarity, detailed balance, $Q$, $h$, $\beta_1$, and simple random walk. A local definition represents each selected walk by its vertex list and derives directed edges from consecutive vertices. The hypothesis $2\leq |V|$ makes $\beta_1$ the paper's second eigenvalue and excludes the one-state junk value of the real supremum used in its definition. Positivity of $\eta$ follows from the chain and walk assumptions; it is not inserted as an extra assumption.

The walk system is universally quantified: the theorem concerns every valid selection, rather than one favorable selection. The local definition ignores equal-endpoint choices because they do not cross any $S$-to-$S^{\mathrm c}$ cut; §3B mentions all ordered pairs, so this convention gives a slightly stronger target and is stated explicitly. The cut lemma retains stochasticity and nonnegative stationary weights to keep the flow of unused cut edges nonnegative. The graph companion derives its Markov-chain properties from connectedness rather than assuming them.

The shared vertex-list representation and the cut crossing statement can serve later path-based bounds. Contributions toward positivity and finiteness of congestion, the uniform cut estimate, the bottleneck estimate, and the graph specialization all fit the mission. A definition that forces $\eta>0$ by fiat, or a goal that assumes the bottleneck estimate or Cheeger's inequality, would erase the mathematical content.

Selected references

• Persi Diaconis and Daniel Stroock, Geometric bounds for eigenvalues of Markov chains, Annals of Applied Probability 1(1):36–61, 1991. DOI.
• David A. Levin, Yuval Peres, and Elizabeth L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009, Chapter 13. Book PDF.

Motivation

Markov chain Monte Carlo methods, card-shuffling schemes and randomized counting algorithms all run a Markov chain until its distribution is close to the stationary distribution. The quantity a user needs is a number of steps $n$ after which $P^n(x,\cdot)$ is within a prescribed variation distance of $\pi$. For reversible chains the standard way to get such a number is to bound the eigenvalues of the transition matrix and convert the eigenvalue bound into a variation distance bound.

P. Diaconis and D. Stroock, in Geometric bounds for eigenvalues of Markov chains (Ann. Appl. Probab. 1, 1991), prove geometric (path-counting) bounds on the second largest and the smallest eigenvalue of a reversible chain. Their §1D supplies the conversion step: Proposition 3 bounds the variation distance to stationarity, in discrete and in continuous time, by the eigenvalues. This mission formalizes that proposition. The eigenvalue bounds themselves are the subject of the other missions of this series.

Setting

Let $X$ be a finite set with $m = |X|$ elements and $P(x,y)$ the transition matrix of a Markov chain on $X$: $P(x,y)\ge 0$ and $\sum_y P(x,y) = 1$. The chain is irreducible if every state can be reached from every other state: for all $x,y$ there is $n$ with $P^n(x,y) > 0$. A probability distribution $\pi$ on $X$ is stationary if $\sum_x \pi(x)P(x,y) = \pi(y)$, and the chain is reversible with respect to $\pi$ if

$$\pi(x)P(x,y) = \pi(y)P(y,x)\qquad\text{for all } x,y\in X.$$

For an irreducible chain $\pi(x) > 0$ for every $x$. Reversibility makes $P$ a self-adjoint operator on $L^2(\pi)$, so its eigenvalues are real; they are written

$$1 = \beta_0 > \beta_1 \ge \beta_2 \ge \dots \ge \beta_{m-1} \ge -1,$$

the strict inequality $\beta_0 > \beta_1$ coming from irreducibility. Put $\beta_* = \max(\beta_1, |\beta_{m-1}|)$, the largest modulus of an eigenvalue other than $1$.

The variation distance between probability distributions $\mu$ and $\pi$ on $X$ is

$$\|\mu - \pi\|_{\mathrm{Var}} = \max_{A\subset X}|\mu(A) - \pi(A)| = \tfrac12\sum_{x\in X}|\mu(x)-\pi(x)|.$$

$P^n(x,\cdot)$ is the distribution of the chain after $n$ steps from $x$. The continuous-time chain jumps according to $P$ at the times of a rate-one Poisson process, and has kernel

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

Formalization targets

Goal: Proposition 3, (1.9)

For every $x \in X$ and every $n\in\mathbb N$,

$$4\,\|P^n(x,\cdot)-\pi\|_{\mathrm{Var}}^2 \;\le\; \frac{1-\pi(x)}{\pi(x)}\,\beta_*^{2n}.$$

Milestones

The steps of the paper's proof (p. 42), in order:

1. the two expressions for $\|\cdot\|_{\mathrm{Var}}$ (p. 41), already proved on the platform;
2. the reversibility identity $\frac{1}{\pi(x)}P^{2n}(x,x) = \sum_y (P^n(x,y))^2/\pi(y)$;
3. the Cauchy–Schwarz bound $4\|P^n(x,\cdot)-\pi\|_{\mathrm{Var}}^2 \le \frac{1}{\pi(x)}P^{2n}(x,x) - 1$;
4. the orthogonal diagonalization of a reversible chain, already proved on the platform in the form $P^t(x,y)/\pi(y) = \sum_j f_j(x)f_j(y)\lambda_j^t$ with $(f_j)$ orthonormal in $L^2(\pi)$;
5. the diagonal bound $P^{2n}(x,x) \le \pi(x) + \beta_*^{2n}(1-\pi(x))$.

Companion: Proposition 3, (1.10)

For every $x\in X$ and every $t\in(0,\infty)$,

$$4\,\|P_t(x,\cdot)-\pi\|_{\mathrm{Var}}^2 \;\le\; \frac{1-\pi(x)}{\pi(x)}\,\exp\bigl[-2(1-\beta_1)t\bigr].$$

The paper gives no separate proof of (1.10); it says only that "the continuous time version can be proved by a virtually identical argument".

Significance

Inequality (1.9) is the step that turns an eigenvalue estimate into a mixing-time estimate: if $\beta_* \le 1 - \varepsilon$, then $\|P^n(x,\cdot)-\pi\|_{\mathrm{Var}} \le \delta$ as soon as $n \ge \frac{1}{2\varepsilon}\bigl(\log\frac{1}{4\delta^2} + \log\frac{1-\pi(x)}{\pi(x)}\bigr)$, up to the usual comparison $\log(1/(1-\varepsilon)) \ge \varepsilon$. The examples of the paper's Section 2 use Propositions 1 and 2 to bound $\beta_1$ and $\beta_{m-1}$, and this proposition to translate the bounds into a number of steps. Inequality (1.10) does the same for the continuous-time chain, where only $\beta_1$ is needed because the continuous-time chain has no periodicity.

The result is classical and its proof is short; it is the $\ell^2$ (chi-square) bound on variation distance found in many textbooks, e.g. Levin, Peres and Wilmer, Markov Chains and Mixing Times, Chapter 12. As far as the platform's catalog shows, neither (1.9) nor (1.10) has a machine-checked proof. The platform already has the spectral decomposition of a reversible chain and the identity between the two forms of total variation, both proved; this mission links them to the variation distance bound in the exact form used by the geometric-bounds literature. The diagonal bound (milestone 5) and the reversibility identity (milestone 2) are reusable statements about reversible chains in their own right.

Difficulty

The Cauchy–Schwarz step and the reversibility identity are finite-sum manipulations. The difficulty is in the spectral step. One has to show that, apart from the eigenvalue $1$ (whose eigenfunction is constant and contributes exactly $\pi(x)$ to $P^{2n}(x,x)$), every eigenvalue in the decomposition has modulus at most $\beta_*$, and that the remaining weights at $x$ sum to $1-\pi(x)$. This uses that $1$ is a simple eigenvalue, which needs irreducibility. Without irreducibility the bound fails. A second eigenvalue equal to $1$ would contribute $\Gamma_{xw}^2$ with no decay, while $\beta_*$, a maximum over eigenvalues different from $1$, does not see it.

A naive approach that bounds $|P^n(x,y)-\pi(y)|$ entry by entry and sums gives a factor depending on $|X|$ rather than on $\pi(x)$; the point of (1.9) is that the constant is $(1-\pi(x))/\pi(x)$ only. For (1.10) the matrix $P_t$ is an infinite series in $P$, and the decomposition has to be carried through the series, each eigenvalue $\beta$ contributing $e^{-2(1-\beta)t}$.

Formalization scope

The objects are the published MarkovMixing definitions (Levin–Peres–Wilmer layer): the chain is a real matrix P : Matrix V V ℝ on a Fintype V with IsStochastic P, MarkovMixing.Irreducible P, IsStationary P π (π is a probability vector with πP = π) and DetailedBalance P π. These four hypotheses are the paper's standing assumption of §1A; every statement of the mission carries all of them, and no other hypothesis.

• $\|P^n(x,\cdot)-\pi\|_{\mathrm{Var}}$ is tvDist (rowDist P n x) π, the supremum over subsets; $P_t(x,\cdot)$ is heatKernel P t x.
• $\beta_*$ is lambdaStar P, the supremum of $|\lambda|$ over real eigenvalues $\lambda \ne 1$; $\beta_1$ is lambdaTwo P, the supremum of real eigenvalues $\lambda\ne1$. For an irreducible reversible chain these are the paper's $\max(\beta_1,|\beta_{m-1}|)$ and $\beta_1$.
• On a one-point space the eigenvalue sets are empty and both quantities are the junk value $0$; both sides of (1.9) and (1.10) are then $0$, so no hypothesis $|X|\ge 2$ is added.
• $n\in\mathbb N$ includes $n = 0$, where (1.9) reads $4(1-\pi(x))^2 \le (1-\pi(x))/\pi(x)$, a true inequality. The time in (1.10) is strictly positive, as in the paper.
• Positivity of $\pi$ is not a hypothesis: it follows from irreducibility and stationarity.

A formalization that assumed milestone 3 or milestone 5 as a hypothesis of the goal, or that replaced $\beta_*$ by a free parameter bounded by hypothesis, would trivialize the goal and is excluded.

Needed infrastructure: finite-dimensional spectral theory for self-adjoint operators on $L^2(\pi)$ (available through the proved MarkovMixing.spectral_representation), simplicity of the eigenvalue $1$ for irreducible chains, Cauchy–Schwarz for finite sums, and termwise manipulation of the Poisson series for (1.10). Proofs of any milestone, and of the simplicity of the top eigenvalue as a separate lemma, are welcome.

Selected references

• P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017 (Lemma 12.2, Proposition 4.2). https://doi.org/10.1090/mbk/107

Why reversibility

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1.8 (p. 23)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first $n$ rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret $O(d\sqrt n\log^{3/2} n)$ with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension $d \ge 1$ and an unknown parameter $\theta_* \in \mathbb R^d$. In round $t = 1, 2, \dots$ the learner is given a nonempty decision set $D_t \subseteq \mathbb R^d$, chooses $X_t \in D_t$, and observes the reward

$$Y_t = \langle X_t, \theta_* \rangle + \eta_t .$$

There is a filtration $\{F_t\}_{t \ge 0}$ such that $X_t$ is $F_{t-1}$-measurable and $\eta_t$ is $F_t$-measurable and conditionally $R$-sub-Gaussian: $\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)$ for all $\lambda \in \mathbb R$, with $R \ge 0$ fixed.

For a regularization parameter $\lambda > 0$ let $\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\top$ and let $\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_s$ be the regularized least-squares estimate. With $\|v\|_A = \sqrt{v^\top A v}$ and a known bound $\|\theta_*\|_2 \le S$, the confidence ellipsoid is

$$C_t = \Big\{\theta : \|\widehat\theta_t - \theta\|_{\overline V_t} \le R\sqrt{2\log\big(\det(\overline V_t)^{1/2}\det(\lambda I)^{-1/2}/\delta\big)} + \lambda^{1/2}S\Big\}.$$

The OFUL algorithm chooses, in round $t$, a pair $(X_t, \widetilde\theta_t)$ maximizing $\langle x, \theta \rangle$ over $D_t \times C_{t-1}$. The pseudo-regret is $R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangle$, where $\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle$.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If $\|X_t\|_2 \le L$, $\langle x, \theta_*\rangle \in [-1,1]$ for all $x \in D_t$, and $\lambda \ge \max(1, L^2)$, then for every $\delta > 0$, with probability at least $1 - \delta$,

$$\forall n \ge 0, \quad R_n \le 4\sqrt{nd\log(\lambda + nL^2/d)}\Big(\lambda^{1/2}S + R\sqrt{2\log(1/\delta) + d\log(1 + nL^2/(\lambda d))}\Big).$$

Milestone: Theorem 1, the self-normalized bound

For any positive definite $V$, $\overline V_t = V + \sum_{s\le t}X_sX_s^\top$ and $S_t = \sum_{s \le t}\eta_sX_s$: with probability at least $1-\delta$, for all $t \ge 0$,

$$\|S_t\|^2_{\overline V_t^{-1}} \le 2R^2\log\big(\det(\overline V_t)^{1/2}\det(V)^{-1/2}/\delta\big).$$

Milestones: Theorem 2, the confidence ellipsoids

With probability at least $1 - \delta$, $\theta_* \in C_t$ for all $t \ge 0$ (first claim). If $\|X_t\|_2 \le L$, then with probability at least $1-\delta$, for all $t$, $\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S$ (second claim, stated here for $d \ge 2$).

Significance

Theorem 3 bounds the regret of OFUL by $O(d\sqrt n\log n)$ with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases $V = \lambda I$, $R = 1$, $\delta < 1$ of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence $X_t$ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix $\overline V_t$, which is itself built from the adaptively chosen actions; a bound for each fixed $t$ does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $\|x\|_A$ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed $t+1$ for $t : ℕ$, so sums over $s \le t$ are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy $R^2$) requires; this is an added hypothesis. Every "with probability at least $1-\delta$, for all $t$" is stated as an outer-measure bound $\le \delta$ on the failure event, with the time quantifier inside the event. $\det(\cdot)^{1/2}$ is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes $\langle x,\theta\rangle$ over $D_t \times C_{t-1}$, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward $\langle x^*_t, \theta_*\rangle$ is the supremum over $D_t$, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed $nL/d$ is replaced by $nL^2/d$, which is what the determinant–trace bound $\det\overline V_n \le (\lambda + nL^2/d)^d$ gives; for $L \le 1$ the corrected bound implies the printed one. The hypothesis $\lambda \ge \max(1, L^2)$ is added: for $\lambda < 1$ the printed logarithm can be negative, and the printed bound would then assert $R_n \le 0$. In the second claim of Theorem 2, $d \ge 2$ is added, because at $d = 1$ the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if $\theta_* \in C_{t-1}$ for all $t$ then $R_n \le \dots$". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same $\delta$ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on $\mathbb R^d$, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general $V$ and $R$, and reusable determinant lemmas are all welcome.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401

Motivation

A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.

Setting

A random variable $X$ with mean $\mu=\mathbb E[X]$ is sub-Gaussian with parameter $\sigma$ (Definition 2.2) if $\mathbb E[e^{\lambda(X-\mu)}]\le e^{\sigma^2\lambda^2/2}$ for all $\lambda\in\mathbb R$; it is sub-exponential with parameters $(\nu,\alpha)$ (Definition 2.7, a strictly milder condition) if the same bound holds only for $|\lambda|<1/\alpha$, with the convention $1/0=+\infty$ so that $\alpha=0$ recovers the sub-Gaussian case exactly.

A sequence $\{D_k\}_{k\ge1}$, adapted to a filtration $\{\mathcal F_k\}$, is a martingale difference sequence if each $D_k$ is $\mathcal F_k$-measurable and $\mathbb E[D_k\mid\mathcal F_{k-1}]=0$. Such sequences arise throughout statistics via the Doob martingale construction: given a function $f$ of independent variables $X_1,\dots,X_n$, setting $D_k:=\mathbb E[f(X)\mid X_1,\dots,X_k]-\mathbb E[f(X)\mid X_1,\dots,X_{k-1}]$ telescopes to $f(X)-\mathbb E[f(X)]=\sum_k D_k$, converting a deviation question about $f(X)$ into a martingale concentration question.

A function $f:\mathbb R^n\to\mathbb R$ is $L$-Lipschitz with respect to the Euclidean norm if $|f(x)-f(y)|\le L\|x-y\|_2$ for all $x,y$ (Eq. (2.38)).

Formalization targets

Goal — Theorem 2.26 (Gaussian concentration of Lipschitz functions)

Let $(X_1,\dots,X_n)$ be i.i.d. standard Gaussian and $f$ be $L$-Lipschitz with respect to the Euclidean norm. Then $f(X)-\mathbb E[f(X)]$ is sub-Gaussian with parameter at most $L$, and hence

$$\mathbb P[|f(X)-\mathbb E[f(X)]|\ge t] \;\le\; 2e^{-t^2/2L^2} \qquad \text{for all } t\ge 0.$$

The bound is dimension-free: it depends on $n$ only through $f$'s Lipschitz constant, not the ambient dimension itself.

Milestone — Lemma 2.27 (Gaussian interpolation identity)

For any differentiable $f$ and convex $\varphi$, $\mathbb E[\varphi(f(X)-\mathbb E[f(X)])] \le \mathbb E[\varphi(\tfrac\pi2\langle\nabla f(X),Y\rangle)]$ for $X,Y\sim N(0,I_n)$ independent — the interpolation identity Theorem 2.26's proof is built on.

Milestone — Theorem 2.19 (martingale Bernstein bound)

Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound $\mathbb E[e^{\lambda D_k}\mid\mathcal F_{k-1}]\le e^{\lambda^2\nu_k^2/2}$ for $|\lambda|<1/\alpha_k$, the sum $\sum_k D_k$ is itself sub-exponential with parameters $\big(\sqrt{\sum_k\nu_k^2},\ \max_k\alpha_k\big)$, and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.

Significance

Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field — the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform (azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz concentration is separately significant: it is the tool behind dimension-free operator-norm bounds for random matrices, concentration of the empirical spectral distribution, and much of the machinery of Chapters 5 and 6 of the same book.

Formalizing it. No faithful prior art exists on the platform for either the martingale Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz concentration" returned no hits; the existing Vershynin-book item HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused from the platform's existing, already-proved formalizations.

Difficulty

The naive approach to Theorem 2.26 — try to bound $f(X)-\mathbb E[f(X)]$ directly via a Lipschitz-type argument in $\mathbb R^n$ — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an $\varepsilon$-net of the domain) picks up a factor that grows with $n$. The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity $f(X)-\mathbb E[f(X)]$ with the linear, and hence exactly computable, Gaussian quantity $\langle\nabla f(X),Y\rangle$, at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly $n$ times while keeping track of the interplay between the two parameters $\nu_k,\alpha_k$ per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.

Formalization scope

Expectations are Bochner integrals against an explicit probability measure, with integrability required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner integral silently returns $0$ for a non-integrable function, which this mission's definitions rule out as a trivializing formalization). The sub-exponential condition's domain restriction |λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention for the degenerate sub-Gaussian case.

"$X,Y\sim N(0,I_n)$ independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's HasGaussianLaw predicate together with explicit coordinatewise mean-zero and identity-covariance hypotheses, which together pin down the standard multivariate normal law, plus IndepFun. The inner product $\langle\nabla f(X),Y\rangle$ is realized as fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to $Y(\omega)$ — equal to $\langle\nabla f(X(\omega)),Y(\omega)\rangle$ by the Riesz representation of the gradient on a Hilbert space, avoiding the need to separately construct a gradient vector field.

Theorem 2.19's printed parameter pair for part (a), "$(\sum_k\nu_k^2,\alpha_*)$," is formalized as $(\sqrt{\sum_k\nu_k^2},\alpha_*)$: Definition 2.7 parametrizes the sub-exponential MGF bound by $\nu$ (with $\nu^2$ appearing in the exponent), so a literal transcription of the printed pair's first entry would silently square the effective parameter and make part (a), read literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full derivation.

Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 2.
• K. Azuma, "Weighted sums of certain dependent random variables," Tôhoku Mathematical Journal, 19:357–367, 1967.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association, 58:13–30, 1963.

Motivation

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

Setting

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

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

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

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

Formalization targets

Goal

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

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

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

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

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

Formalization targets

Goal

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

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

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

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

Formalization targets

Goal

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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