Section 7.1.2 -- the diameter bound

Proved

MarkovMixing.diameter_lower_bound

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Let $P$ be an irreducible, aperiodic Markov chain on a finite state space $V$ with stationary distribution $\pi$ . The transition graph of $P$ joins two distinct states $x\ne y$ whenever the chain can cross between them in one step in either direction ( $P(x,y)>0$ or $P(y,x)>0$ ); write $\rho(x,y)$ for the graph distance in this graph — the least number of steps needed to travel from $x$ to $y$ . For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ .

The theorem (the diameter bound, §7.1.2, display (7.3) of Levin–Peres–Wilmer) asserts: for every tolerance $\varepsilon<\tfrac12$ and every pair of states $x_0,y_0$ ,

\rho(x_0,y_0)\;\le\;2\,t_{\mathrm{mix}}(\varepsilon).

Equivalently, the mixing time is at least half the diameter of the transition graph: started at two states at distance $\rho$ , for $t<\rho/2$ the two time- $t$ distributions occupy disjoint balls and cannot both be within $\varepsilon<\tfrac12$ of the same $\pi$ .

Preamble

import Definitions.Def_mm_lower

Formal statement

namespace MarkovMixing

/-- **§7.1.2, Eq. (7.3)** (LPW), the diameter bound: for `ε < 1/2`, the
mixing time is at least half the graph distance between any two states (in
particular, at least half the diameter of the chain). -/
theorem diameter_lower_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hap : Aperiodic P) (π : V → ℝ) (hπ : IsStationary P π)
    (ε : ℝ) (hε : 0 < ε) (hε2 : ε < 1 / 2) (x₀ y₀ : V) :
    (transGraph P).dist x₀ y₀ ≤ 2 * mixingTime P π ε := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 7.1.2, Eq. (7.3), p. 88

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `diameter_lower_bound`

Let $V$ be a finite, nonempty type with decidable equality, let $P$ be a $V \times V$ real matrix, and let $\pi : V \to \mathbb{R}$ . The hypotheses are:

Stochastic: $P_{x,y} \ge 0$ for all $x, y$ , and $\sum_y P_{x,y} = 1$ for every $x$ .
Irreducible (as defined in this bundle): for every ordered pair $x, y$ there exists a natural number $t \ge 0$ with $(P^t)_{x,y} > 0$ . (Because $t = 0$ is permitted and $P^0 = I$ , the requirement is automatic for $x = y$ .)
Aperiodic (as defined in this bundle): every state $x$ has period $1$ , where the period of $x$ is the supremum in $\mathbb{N}$ (with $\sup = 0$ for a set with no upper bound) of the set of $d \in \mathbb{N}$ dividing every $t \ge 1$ with $(P^t)_{x,x} > 0$ .
Stationarity: $\pi$ is a probability distribution ( $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ ) and is invariant as a row vector: $\pi P = \pi$ .
$\varepsilon$ is a real number with $0 < \varepsilon < \tfrac{1}{2}$ (both strict).
$x_0, y_0$ are two arbitrary (universally quantified) states of $V$ .

Two graph-theoretic and mixing-theoretic quantities appear in the conclusion. First, the transition graph of $P$ is the simple undirected loopless graph $G_P$ on $V$ in which distinct vertices $x \neq y$ are adjacent exactly when $P_{x,y} > 0$ or $P_{y,x} > 0$ (the relation "positive transition probability" is symmetrized, and loops are discarded regardless of diagonal entries). The quantity $d_{G_P}(x_0, y_0)$ is the graph distance in $G_P$ : the least length of a walk from $x_0$ to $y_0$ , a natural number, with the Mathlib convention that the distance is $0$ when no walk connects the two vertices (as well as when $x_0 = y_0$ ). Second, the mixing time is

t_{\mathrm{mix}}(\varepsilon) := \min\Big\{ t \in \mathbb{N} \;:\; \max_{x \in V}\; d_{TV}\big((P^t)_{x,\cdot},\, \pi\big) \le \varepsilon \Big\},

where $d_{TV}(\mu, \nu) := \sup_{A \subseteq V} \big|\sum_{x \in A}\mu(x) - \sum_{x \in A}\nu(x)\big|$ (the standard total-variation distance, expressed as a supremum over subsets, with no extra factor $\tfrac12$ ), $(P^t)_{x,\cdot}$ denotes the $x$ -th row of $P^t$ , and by the $\mathbb{N}$ -infimum convention $t_{\mathrm{mix}}(\varepsilon) = 0$ if no time $t$ achieves distance $\le \varepsilon$ .

The conclusion is the inequality of natural numbers

d_{G_P}(x_0, y_0) \;\le\; 2\, t_{\mathrm{mix}}(\varepsilon),

i.e. the graph distance between the two chosen states in the symmetrized positive-transition graph is at most twice the $\varepsilon$ -mixing time. Since $x_0$ and $y_0$ range over all pairs of states, the statement is equivalent to bounding the diameter-type quantity $\max_{x,y} d_{G_P}(x,y)$ by $2\,t_{\mathrm{mix}}(\varepsilon)$ — subject to the caveats above that disconnected pairs contribute distance $0$ rather than infinity, and that an "unmixable" chain contributes mixing time $0$ rather than infinity.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Section 7.1.2 -- the diameter bound

Read-back: diameter_lower_bound

Read-back: `diameter_lower_bound`