Lemma 13.22 -- comparison of Dirichlet forms

Disproved

MarkovMixing.dirichlet_comparison

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

markov-chainsmixing-timesprobability

Let $P$ and $\tilde P$ be two Markov chains on the same finite state space $V$ with at least two states, with stationary distributions $\pi$ and $\tilde\pi$ respectively, each reversible (detailed balance: $\pi(x)P(x,y)=\pi(y)P(y,x)$ , and likewise for $\tilde P,\tilde\pi$ ), with $\tilde\pi$ strictly positive. Each chain carries a Dirichlet form and a spectral gap:

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

where $\lambda_2$ is the largest eigenvalue different from $1$ (an eigenvalue being a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$ ); write $\tilde{\mathcal E}$ and $\tilde\gamma$ for the corresponding quantities of $\tilde P$ .

The theorem (Lemma 13.22 of Levin–Peres–Wilmer, the comparison of Dirichlet forms) asserts: if for some constant $B>0$ the forms compare as $\tilde{\mathcal E}(f)\le B\,\mathcal E(f)$ for every function $f:V\to\mathbb R$ , then the gaps compare as

\tilde\gamma\;\le\;\Bigl(\max_{x\in V}\frac{\pi(x)}{\tilde\pi(x)}\Bigr)\,B\,\gamma.

This is the comparison method: a spectral gap estimate for one chain transfers to any chain whose Dirichlet form it dominates, at the price of the constant $B$ and the worst ratio of stationary masses. It is the engine behind the shuffle bounds of Mission V, where a complicated shuffle is compared with random transpositions.

Retired — this statement is false as written

Replaced by MarkovMixing.dirichlet_comparison_irreducible. Disproved by chenmin (submission dfa7a37a-5a8c-4a6a-9f82-3217070c1f36, accepted).

The statement omits irreducibility of the two chains. lambdaTwo is the supremum of the eigenvalues different from $1$ , which is LPW's $\lambda_2$ — the second eigenvalue counted with multiplicity — only when $1$ is a simple eigenvalue, i.e. when the chain is irreducible. Without it the set can be empty; $\sup\emptyset=0$ in Lean, so both spectral gaps read $1$ . For $P=\tilde P=I$ on two states both Dirichlet forms vanish identically, so the comparison hypothesis holds for every $B>0$ , while the conclusion fails already at $B=1/100$ .

LPW prove Lemma 13.22 through the variational characterization of Remark 13.13, which is a statement about irreducible chains. Do not re-formalize this statement without irreducibility.

Preamble

import Definitions.Def_mm_spectral

Formal statement

namespace MarkovMixing

/-- **Lemma 13.22** (LPW), the comparison of Dirichlet forms: if
`Ẽ(f) ≤ B E(f)` for all `f`, then the spectral gaps satisfy
`γ̃ ≤ [max_x π(x)/π̃(x)] B γ`. -/
theorem dirichlet_comparison {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (hV : 2 ≤ Fintype.card V) (P P' : Matrix V V ℝ) (hP : IsStochastic P) (hP' : IsStochastic P')
    (π π' : V → ℝ) (hπ : IsStationary P π) (hπ' : IsStationary P' π')
    (hrev : DetailedBalance P π) (hrev' : DetailedBalance P' π')
    (hpos' : ∀ x : V, 0 < π' x)
    (B : ℝ) (hB : 0 < B)
    (hcomp : ∀ f : V → ℝ, dirichletForm P' π' f ≤ B * dirichletForm P π f) :
    spectralGap P' ≤ (⨆ x : V, π x / π' x) * B * spectralGap 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.4, Lemma 13.22, p. 180

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$ and $P'$ be two $V \times V$ real matrices, both stochastic (all entries nonnegative and every row summing to one). Let $\pi, \pi' : V \to \mathbb{R}$ be stationary distributions for $P$ and $P'$ respectively — each is nonnegative, sums to one over $V$ , and satisfies $\pi P = \pi$ (resp. $\pi' P' = \pi'$ ) as a row vector — and assume both pairs satisfy detailed balance: $\pi(x) P(x,y) = \pi(y) P(y,x)$ and $\pi'(x) P'(x,y) = \pi'(y) P'(y,x)$ for all $x, y \in V$ . Assume additionally that $\pi'$ is strictly positive everywhere ( $\pi'(x) > 0$ for all $x$ ; no such positivity is assumed for $\pi$ ), and that there is a real constant $B > 0$ such that for every function $f : V \to \mathbb{R}$ the Dirichlet forms compare as

\mathcal{E}'(f) \;\le\; B \, \mathcal{E}(f), \qquad \text{where} \quad \mathcal{E}(f) = \frac{1}{2}\sum_{x}\sum_{y} \big(f(x)-f(y)\big)^2\, \pi(x)\,P(x,y)

and $\mathcal{E}'(f)$ is defined identically with $\pi', P'$ in place of $\pi, P$ (note the Dirichlet form of $P'$ is dominated by $B$ times that of $P$ , in that direction). The theorem then asserts the inequality

\gamma' \;\le\; \left( \sup_{x \in V} \frac{\pi(x)}{\pi'(x)} \right) \cdot B \cdot \gamma,

where $\gamma = 1 - \lambda_2(P)$ and $\gamma' = 1 - \lambda_2(P')$ are the spectral gaps: here $\lambda_2(Q)$ denotes the supremum of the set of real numbers $\lambda \ne 1$ for which there exists a not-identically-zero function $f : V \to \mathbb{R}$ with $Qf = \lambda f$ pointwise ( $\sum_y Q(x,y) f(y) = \lambda f(x)$ for all $x$ ); by the real-supremum convention this supremum equals $0$ (making the corresponding gap equal $1$ ) if the eigenvalue set is empty or unbounded above. The prefactor $\sup_x \pi(x)/\pi'(x)$ is a finite maximum over the states of $V$ ; each quotient is well defined since $\pi'(x) > 0$ . Note that neither chain is assumed irreducible or aperiodic, and the conclusion bounds the spectral gap of $P'$ (the chain whose Dirichlet form is on the smaller side of the comparison hypothesis) by the ratio-weighted multiple $B$ of the spectral gap of $P$ .

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