Theorem 13.14 -- the Cheeger inequality

Proved

MarkovMixing.cheeger_inequality

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a finite state space $V$ with at least two states, reversible with respect to its stationary distribution $\pi$ (detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$ ). Two quantities measure how quickly the chain can move:

the bottleneck constant $\Phi_\star=\min\bigl\{\Phi(S):\varnothing\ne S\subseteq V,\ \pi(S)\le\tfrac12\bigr\}$ , where $\Phi(S)=\sum_{x\in S,\,y\notin S}\pi(x)P(x,y)\,/\,\pi(S)$ is the conditional probability at stationarity of escaping the set $S$ in one step — a geometric, cut-based quantity;
the spectral gap $\gamma=1-\lambda_2$ , where $\lambda_2$ is the largest eigenvalue of $P$ different from $1$ (an eigenvalue being a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$ ) — an analytic quantity.

The theorem (Theorem 13.14 of Levin–Peres–Wilmer; Jerrum–Sinclair, Lawler–Sokal — the discrete Cheeger inequality, capstone of Chapters 12–13) asserts:

$\dfrac{\Phi_\star^2}{2}\;\le\;\gamma$ ;
$\gamma\;\le\;2\,\Phi_\star$ .

Bottlenecks and spectral gaps control each other up to a square: a chain mixes rapidly exactly when it has no bottleneck. This equivalence is the backbone of the Markov-chain approach to approximate counting and of expander graph theory.

Preamble

import Definitions.Def_mm_spectral

Formal statement

namespace MarkovMixing

/-- **Theorem 13.14** (Jerrum–Sinclair, Lawler–Sokal; LPW), the capstone of
Chapters 12–13: the spectral gap and the bottleneck ratio of a reversible
chain satisfy `Φ⋆²/2 ≤ γ ≤ 2Φ⋆`. -/
theorem cheeger_inequality {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (hV : 2 ≤ Fintype.card V) (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) (hrev : DetailedBalance P π) :
    bottleneckStar P π ^ 2 / 2 ≤ spectralGap P ∧
    spectralGap P ≤ 2 * bottleneckStar 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 13.3, Theorem 13.14, Eq. (13.13), p. 177

Read-back

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

Let $V$ be a finite nonempty type (with decidable equality) containing at least two elements ( $2 \le |V|$ ), and let $P$ be a $V \times V$ matrix of real numbers satisfying: (i) stochasticity — every entry $P(x,y) \ge 0$ and every row sums to one, $\sum_y P(x,y) = 1$ ; (ii) irreducibility — for every pair of states $x, y$ there is a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (the exponent $t = 0$ is permitted, and since $P^0$ is the identity this makes the condition automatic when $x = y$ ); (iii) there is a function $\pi : V \to \mathbb{R}$ that is a stationary distribution — $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ , and $\pi P = \pi$ as a row vector — and (iv) the pair $(P, \pi)$ satisfies detailed balance: $\pi(x)\,P(x,y) = \pi(y)\,P(y,x)$ for all $x, y \in V$ . The theorem then asserts the two-sided bound

\frac{\Phi_*^2}{2} \;\le\; \gamma \qquad \text{and} \qquad \gamma \;\le\; 2\,\Phi_*,

where the two quantities are defined as follows. The bottleneck ratio (conductance) $\Phi_*$ is the infimum

\Phi_* \;=\; \inf_{\substack{S \subseteq V,\ S \ne \emptyset \\ \pi(S) \le 1/2}} \; \frac{\displaystyle\sum_{x \in S} \sum_{y \notin S} \pi(x)\,P(x,y)}{\displaystyle\sum_{x \in S} \pi(x)},

taken over all nonempty subsets $S$ of $V$ with $\pi(S) := \sum_{x \in S} \pi(x) \le \tfrac12$ ; note that by the total-function division convention, any set with $\pi(S) = 0$ contributes ratio $0/0 = 0$ to this infimum, and the real-valued infimum is $0$ by convention if the family of admissible sets were empty or the ratios unbounded below. The spectral gap is $\gamma = 1 - \lambda_2$ , where $\lambda_2$ is the supremum of the set of real numbers $\lambda \ne 1$ that are eigenvalues of $P$ in the sense that there exists a function $f : V \to \mathbb{R}$ , not identically zero, with $Pf = \lambda f$ (i.e. $\sum_y P(x,y) f(y) = \lambda f(x)$ for all $x$ ); this real supremum is $0$ by convention if the set of such eigenvalues is empty or unbounded above, in which case $\gamma = 1$ . No aperiodicity is assumed, and the conclusion is a conjunction of the two inequalities: $\Phi_*^2 / 2 \le 1 - \lambda_2$ and $1 - \lambda_2 \le 2\,\Phi_*$ .

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