Lemmas 13.11 and 13.12 -- the variational characterization of the gap

Proved

MarkovMixing.dirichlet_gap

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)$ ). Among the eigenvalues of $P$ — the real $\lambda$ admitting a nonzero $f$ with $Pf=\lambda f$ — let $\lambda_2$ be the largest eigenvalue different from $1$ , and let $\gamma=1-\lambda_2$ be the spectral gap. For functions $f:V\to\mathbb R$ write $\mathbb E_\pi(f)=\sum_xf(x)\pi(x)$ for the mean, $\langle f,f\rangle_\pi=\sum_xf(x)^2\pi(x)$ for the squared $\ell^2(\pi)$ -norm, and

\mathcal E(f)=\frac12\sum_{x,y}\bigl[f(x)-f(y)\bigr]^2\,\pi(x)P(x,y)

for the Dirichlet form — the average squared local variation of $f$ along the chain's transitions.

The theorem (Lemmas 13.11 and 13.12 of Levin–Peres–Wilmer) asserts:

the spectral gap is the minimal Dirichlet energy over centred unit-norm functions: $\gamma=\inf\bigl\{\mathcal E(f)\;:\;\mathbb E_\pi(f)=0,\ \langle f,f\rangle_\pi=1\bigr\}$ ;
the infimum is attained by some such $f$ (an eigenfunction for $\lambda_2$ ).

This variational characterization lets one bound the gap from above by exhibiting any single test function, and from below by functional inequalities — the mechanism driving the Cheeger inequality and the comparison method of this mission.

Preamble

import Definitions.Def_mm_spectral

Formal statement

namespace MarkovMixing

/-- **Lemmas 13.11 and 13.12** (LPW): the spectral gap of a reversible chain
is the minimal Dirichlet energy over functions of mean zero and unit
`ℓ²(π)`-norm, and the minimum is attained. -/
theorem dirichlet_gap {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 π) :
    spectralGap P =
      sInf {e : ℝ | ∃ f : V → ℝ, distExp π f = 0 ∧ innerPi π f f = 1 ∧
        e = dirichletForm P π f} ∧
    ∃ f : V → ℝ, distExp π f = 0 ∧ innerPi π f f = 1 ∧
      spectralGap P = dirichletForm P π f := 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, Lemmas 13.11-13.12, pp. 175-176

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$ real matrix that is stochastic (every entry $P(x,y) \ge 0$ and every row sums to one, $\sum_y P(x,y) = 1$ ) and irreducible in the sense that for all states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (the exponent $t = 0$ is allowed, and since $P^0$ is the identity the condition is automatic for $x = y$ ). Let $\pi : V \to \mathbb{R}$ be a stationary distribution — $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ , and $\pi P = \pi$ as a row vector — and assume detailed balance: $\pi(x) P(x,y) = \pi(y) P(y,x)$ for all $x, y$ . Define the spectral gap $\gamma = 1 - \lambda_2$ , where $\lambda_2$ is the supremum of the set of real numbers $\lambda \ne 1$ that admit a nonzero real function $f : V \to \mathbb{R}$ with $Pf = \lambda f$ (pointwise, $\sum_y P(x,y) f(y) = \lambda f(x)$ for all $x$ ); by the real-supremum convention this supremum is $0$ if the set of such eigenvalues is empty or unbounded above. Define also, for $f : V \to \mathbb{R}$ , the mean $\mathbb{E}_\pi[f] = \sum_x f(x)\,\pi(x)$ , the $\pi$ -weighted inner product $\langle f, f \rangle_\pi = \sum_x f(x)^2\,\pi(x)$ , and the Dirichlet form

\mathcal{E}(f) \;=\; \frac{1}{2} \sum_{x \in V} \sum_{y \in V} \big(f(x) - f(y)\big)^2\, \pi(x)\, P(x,y).

The theorem asserts the conjunction of two claims. First, the spectral gap equals the infimum of the Dirichlet form over normalized mean-zero functions:

\gamma \;=\; \inf\left\{ \mathcal{E}(f) \;:\; f : V \to \mathbb{R},\ \mathbb{E}_\pi[f] = 0,\ \langle f, f \rangle_\pi = 1 \right\},

where the infimum is the real-valued infimum of the set of attained values $\mathcal{E}(f)$ , which by convention equals $0$ if that set were empty (i.e. if no function satisfied both constraints — note the normalization $\langle f, f \rangle_\pi = 1$ can fail to be satisfiable only in degenerate situations, e.g. it forces $\pi$ to charge some point) or unbounded below. Second, the infimum is attained: there exists a function $f : V \to \mathbb{R}$ with $\mathbb{E}_\pi[f] = 0$ and $\langle f, f \rangle_\pi = 1$ such that $\gamma = \mathcal{E}(f)$ exactly. No aperiodicity assumption is made, and both claims are equalities (not merely inequalities in one direction).

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