Theorem 7.3 -- the bottleneck ratio bound

Proved

MarkovMixing.bottleneck_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 edge measure $Q(x,y)=\pi(x)P(x,y)$ is the stationary flow along $(x,y)$ ; the bottleneck ratio of a set of states $S$ is

\Phi(S)=\frac{Q(S,S^c)}{\pi(S)}=\frac{\sum_{x\in S}\sum_{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\}$ . The mixing time $t_{\mathrm{mix}}$ is the first $t$ at which $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\tfrac14$ , with $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ the total variation distance.

The theorem (Theorem 7.3 of Levin–Peres–Wilmer, the capstone of Chapter 7) asserts:

t_{\mathrm{mix}}\;\ge\;\frac{1}{4\,\Phi_\star}.

A chain with a bottleneck — a half-space it leaves only reluctantly — mixes slowly: started inside such a set, the chain needs order $1/\Phi(S)$ steps to transfer the requisite mass out. This is the qualitative converse of the Cheeger inequality of Mission VII.

Preamble

import Definitions.Def_mm_lower

Formal statement

namespace MarkovMixing

/-- **Theorem 7.3** (LPW), the bottleneck-ratio bound and capstone of
Chapter 7: `t_mix ≥ 1/(4 Φ⋆)`. -/
theorem bottleneck_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 π) :
    (4 * bottleneckStar P π)⁻¹ ≤ (tMix 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.2, Theorem 7.3, p. 89

Read-back

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

Read-back: `bottleneck_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}$ , under the following hypotheses.

Stochastic: $P_{x,y} \ge 0$ for all $x, y$ , and every row of $P$ sums to $1$ .
Irreducible (as defined in this bundle): for every ordered pair $x, y$ there is a natural number $t \ge 0$ with $(P^t)_{x,y} > 0$ ; since $t = 0$ is allowed and $P^0 = I$ , this is automatic for $x = y$ .
Aperiodic (as defined in this bundle): every state $x$ has period $1$ , the period being the supremum in $\mathbb{N}$ (with the convention $\sup = 0$ for a set without an upper bound) of the set of $d$ dividing every $t \ge 1$ with $(P^t)_{x,x} > 0$ .
Stationarity: $\pi$ is a probability distribution ( $\pi \ge 0$ pointwise, $\sum_x \pi(x) = 1$ ) with $\pi P = \pi$ as row vectors.

Two custom quantities appear in the conclusion. The bottleneck constant is

\Phi_\ast := \inf\left\{ \frac{\sum_{x \in S} \sum_{y \notin S} \pi(x)\, P_{x,y}}{\sum_{x \in S} \pi(x)} \;:\; S \subseteq V,\ S \neq \emptyset,\ \sum_{x \in S} \pi(x) \le \tfrac{1}{2} \right\},

the infimum, over all nonempty subsets $S$ of $V$ whose $\pi$ -mass is at most $\tfrac12$ (non-strict), of the ratio of the flow $\sum_{x\in S,\, y\in S^c}\pi(x)P_{x,y}$ out of $S$ to the mass $\pi(S)$ ; each ratio uses the real-division convention that division by zero gives $0$ (so a subset with $\pi(S) = 0$ contributes ratio $0$ ), and if no subset satisfies the two side conditions the infimum defaults to the junk value $0$ . The mixing time is

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

where $d_{TV}(\mu,\nu) := \sup_{A \subseteq V} \big|\sum_{x\in A}\mu(x) - \sum_{x\in A}\nu(x)\big|$ is the total-variation distance written as a supremum of mass discrepancies over subsets (no extra factor $\tfrac12$ ), $(P^t)_{x,\cdot}$ is the $x$ -th row of $P^t$ , the threshold is the fixed constant $\tfrac14$ , and by the $\mathbb{N}$ -infimum convention $t_{\mathrm{mix}} = 0$ if no time meets the threshold.

The theorem asserts the single real inequality

\frac{1}{4\, \Phi_\ast} \;\le\; t_{\mathrm{mix}},

with $t_{\mathrm{mix}}$ cast from $\mathbb{N}$ to $\mathbb{R}$ and with the real-inversion convention $0^{-1} = 0$ : if $\Phi_\ast = 0$ (in particular in the degenerate situation where no nonempty $S$ has $\pi(S) \le \tfrac12$ , or where the infimum genuinely vanishes) the left-hand side is $0$ and the claim reduces to the trivial $0 \le t_{\mathrm{mix}}$ . The inequality is non-strict, and the bound has the specific constant $\tfrac{1}{4}$ : the mixing time at accuracy $\tfrac14$ is at least $\big(4\,\Phi_\ast\big)^{-1}$ .

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

Theorem 7.3 -- the bottleneck ratio bound

Read-back: bottleneck_lower_bound

Read-back: `bottleneck_lower_bound`