Theorem 12.3 -- mixing is at most relaxation times a log factor

Disproved

MarkovMixing.relaxation_upper

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$ , 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_\star$ be the largest absolute value of an eigenvalue different from $1$ ; the absolute spectral gap is $\gamma_\star=1-\lambda_\star$ and the relaxation time is $t_{\mathrm{rel}}=1/\gamma_\star$ . Write $\pi_{\min}=\min_x\pi(x)$ , and for a tolerance $\varepsilon$ let $t_{\mathrm{mix}}(\varepsilon)$ be the first $t$ with $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance.

The theorem (Theorem 12.3 of Levin–Peres–Wilmer) asserts: for every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\le\;\log\!\Bigl(\frac{1}{\varepsilon\,\pi_{\min}}\Bigr)\,t_{\mathrm{rel}}\;+\;1.

Mixing costs at most a $\log(1/\pi_{\min})$ factor beyond the relaxation time: once the spectral gap is known, a mixing bound follows instantly. (The $+1$ absorbs the rounding of the real-valued bound to an integer time.) The companion theorem gives the matching lower bound $t_{\mathrm{mix}}(\varepsilon)\ge(t_{\mathrm{rel}}-1)\log(1/2\varepsilon)$ .

Retired — this statement is false as written

Replaced by MarkovMixing.relaxation_upper_aperiodic. Disproved by chenmin (submission cf1ada7f-968b-47b8-b2a7-3801ab01c781, accepted).

The statement omits aperiodicity. LPW state Theorem 12.3 for a reversible irreducible chain and read $t_{\mathrm{rel}}=1/\gamma_\star$ in the extended reals, where the periodic case gives $t_{\mathrm{rel}}=\infty$ and the bound is vacuously true. Lean's inversion is total — $0^{-1}=0$ — so for a periodic chain $t_{\mathrm{rel}}$ evaluates to $0$ and the bound collapses to $t_{\mathrm{mix}}(\varepsilon)\le1$ . Simple random walk on the path $0\!-\!1\!-\!2\!-\!3$ is reversible, irreducible and periodic, with $t_{\mathrm{mix}}(3/5)=2$ .

Aperiodicity is the book's own criterion for $\gamma_\star>0$ (Lemma 12.1(iii)); the replacement adds it and is otherwise identical. Do not re-formalize this statement without it.

Preamble

import Definitions.Def_mm_spectral
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Theorem 12.3** (LPW): for a reversible irreducible chain,
`t_mix(ε) ≤ log(1/(ε π_min)) · t_rel + 1`. -/
theorem relaxation_upper {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) (hrev : DetailedBalance P π)
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (mixingTime P π ε : ℝ) ≤
      Real.log (1 / (ε * ⨅ x : V, π x)) * relaxationTime P + 1 := 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 12.2, Theorem 12.3, Eq. (12.9), p. 155

Read-back

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

Read-back: `relaxation_upper`

Let $V$ be a finite, nonempty type with decidable equality. The hypotheses are: $P$ is a $V \times V$ real matrix that is stochastic (all entries $P_{x,y} \ge 0$ , all rows sum to one); $P$ is irreducible in the sense that for every pair $x, y \in V$ there is some natural number $t \ge 0$ (the value $t = 0$ , giving the identity matrix, is allowed) with $(P^t)_{x,y} > 0$ ; $\pi : V \to \mathbb{R}$ is stationary for $P$ , meaning $\pi$ is a probability distribution ( $\pi(x) \ge 0$ for all $x$ , $\sum_x \pi(x) = 1$ — strict positivity of $\pi$ is not assumed) and the row-vector equation $\pi P = \pi$ holds, i.e. $\sum_x \pi(x) P_{x,y} = \pi(y)$ for all $y$ ; $P$ satisfies detailed balance with respect to $\pi$ : $\pi(x) P_{x,y} = \pi(y) P_{y,x}$ for all $x, y$ ; and $\varepsilon$ is a real number with $0 < \varepsilon < 1$ .

The conclusion is the single real inequality

t_{\mathrm{mix}}(\varepsilon) \;\le\; \log\!\Bigl(\frac{1}{\varepsilon \cdot \pi_{\min}}\Bigr) \cdot t_{\mathrm{rel}}(P) \;+\; 1,

where each ingredient has the following literal meaning.

$t_{\mathrm{mix}}(\varepsilon)$ is the natural number $\inf\{t \in \mathbb{N} \mid d(t) \le \varepsilon\}$ , cast into $\mathbb{R}$ ; if no time $t$ achieves $d(t) \le \varepsilon$ , this infimum over the empty set of naturals takes the junk value $0$ . Here $d(t) := \sup_{x \in V} \|(P^t)_{x,\cdot} - \pi\|_{\mathrm{TV}}$ , and for two real-valued functions $\mu, \nu$ on $V$ the "total-variation distance" is defined as $\|\mu - \nu\|_{\mathrm{TV}} := \sup_{A \subseteq V} \bigl|\sum_{x \in A} \mu(x) - \sum_{x \in A} \nu(x)\bigr|$ , the supremum over all (finite) subsets $A$ of $V$ of the absolute difference in mass — with no factor of $\tfrac{1}{2}$ in the definition.
$\pi_{\min} := \inf_{x \in V} \pi(x)$ , the minimum stationary weight (well-defined as a genuine minimum since $V$ is finite and nonempty; it may be $0$ , since positivity of $\pi$ is not hypothesized).
The logarithm is the real natural logarithm, extended by the junk convention $\log s = 0$ for $s \le 0$ ; and $\frac{1}{\varepsilon \cdot \pi_{\min}}$ uses real division with the convention $a/0 = 0$ . In particular, if $\pi_{\min} = 0$ the whole logarithm factor collapses to $\log 0 = 0$ and the right side reduces to $1$ .
$t_{\mathrm{rel}}(P) := \bigl(1 - \lambda_\star(P)\bigr)^{-1}$ , where $\lambda_\star(P)$ is the supremum, in $\mathbb{R}$ , of the set $\{\,|\lambda| \mid \lambda \in \mathbb{R},\ \lambda \ne 1,\ \exists\, f : V \to \mathbb{R},\ f \not\equiv 0,\ P f = \lambda f\,\}$ — the absolute values of all real eigenvalues of $P$ (witnessed by real eigenvectors) other than the value $1$ itself; $\lambda = -1$ is not excluded from this set. The real supremum of an empty set is the junk value $0$ (making $t_{\mathrm{rel}} = 1$ in that case), and real inversion satisfies $0^{-1} = 0$ , so $t_{\mathrm{rel}}(P) = 0$ whenever $\lambda_\star(P) = 1$ . No hypothesis of aperiodicity (or laziness) appears anywhere in the statement.

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 12.3 -- mixing is at most relaxation times a log factor

Retired — this statement is false as written

Read-back: relaxation_upper

Read-back: `relaxation_upper`