Theorem 12.4 -- mixing is at least the relaxation time

Proved

MarkovMixing.relaxation_lower

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$ , 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$ . For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ .

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

t_{\mathrm{mix}}(\varepsilon)\;\ge\;\bigl(t_{\mathrm{rel}}-1\bigr)\,\log\!\Bigl(\frac{1}{2\varepsilon}\Bigr).

A chain cannot mix faster than it relaxes: an eigenfunction with eigenvalue close to $1$ decays like $\lambda_\star^t$ and remains a visible witness against stationarity for about $t_{\mathrm{rel}}$ steps. Together with the companion upper bound $t_{\mathrm{mix}}(\varepsilon)\le\log(1/\varepsilon\pi_{\min})\,t_{\mathrm{rel}}+1$ , this sandwiches the mixing time between $t_{\mathrm{rel}}$ and $t_{\mathrm{rel}}\log(1/\pi_{\min})$ for reversible chains.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 12.4** (LPW): for a reversible, irreducible, aperiodic chain,
`t_mix(ε) ≥ (t_rel − 1) log(1/(2ε))`. -/
theorem relaxation_lower {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 π)
    (hrev : DetailedBalance P π) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (relaxationTime P - 1) * Real.log (1 / (2 * ε)) ≤
      (mixingTime 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 12.2, Theorem 12.4, Eq. (12.12), p. 155

Read-back

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

Let $V$ be a nonempty finite set (with decidable equality) and let $P$ be a real $V \times V$ matrix. The theorem takes the following hypotheses: (1) $P$ is stochastic, meaning every entry satisfies $P_{x,y} \ge 0$ and every row sums to one, $\sum_y P_{x,y} = 1$ ; (2) $P$ is irreducible in the bundle's sense: for every pair of states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)_{x,y} > 0$ — note that $t = 0$ is allowed, so for $x = y$ this is automatic since $P^0$ is the identity; (3) $P$ is aperiodic in the bundle's sense: for every state $x$ , the "period" of $x$ equals $1$ , where the period is defined as the supremum in $\mathbb{N}$ of the set of natural numbers $d$ that divide every element of the return set $\{t \ge 1 : (P^t)_{x,x} > 0\}$ (if the return set is empty, every $d$ is a common divisor, the divisor set is unbounded, and the $\mathbb{N}$ -supremum convention makes the period $0$ , not $1$ ); (4) $\pi : V \to \mathbb{R}$ is a stationary distribution: $\pi$ has nonnegative entries summing to $1$ , and the row vector $\pi$ satisfies $\pi P = \pi$ ; (5) detailed balance holds: $\pi(x)\,P_{x,y} = \pi(y)\,P_{y,x}$ for all $x, y$ ; (6) $\varepsilon$ is a real number with $0 < \varepsilon < 1$ . Under these hypotheses the conclusion is the inequality

\bigl(t_{\mathrm{rel}}(P) - 1\bigr)\,\log\!\frac{1}{2\varepsilon} \;\le\; t_{\mathrm{mix}}(P, \pi, \varepsilon),

where the right side is the natural number $t_{\mathrm{mix}}(P,\pi,\varepsilon) = \inf\{t \in \mathbb{N} : d(t) \le \varepsilon\}$ cast to a real number, with $d(t) = \sup_{x \in V}\, \sup_{A \subseteq V} \bigl|\sum_{y \in A}(P^t)_{x,y} - \sum_{y \in A}\pi(y)\bigr|$ — total variation distance in its supremum-over-subsets form (no factor $\tfrac12$ ), the outer supremum over all starting states; by the $\mathbb{N}$ -infimum convention, if no time $t$ achieves $d(t) \le \varepsilon$ then $t_{\mathrm{mix}} = 0$ . The left side uses the relaxation time $t_{\mathrm{rel}}(P) = (1 - \lambda^\ast(P))^{-1}$ , where $\lambda^\ast(P) = \sup\{\,|\lambda| : \lambda \text{ a real eigenvalue of } P,\ \lambda \ne 1\,\}$ and " $\lambda$ is an eigenvalue" means there exists a nonzero function $f : V \to \mathbb{R}$ with $P f = \lambda f$ (a right eigenvector; only real eigenvalues count, complex ones are invisible to this definition). Degenerate conventions matter here: the real supremum of an empty or unbounded set is $0$ in Lean, so if $P$ has no real eigenvalue other than possibly $1$ then $\lambda^\ast = 0$ ; and if $\lambda^\ast = 1$ then $t_{\mathrm{rel}} = 0^{-1} = 0$ by the real-number convention $1/0 = 0$ . The logarithm is the real natural logarithm; note that for $\varepsilon > \tfrac12$ the factor $\log\frac{1}{2\varepsilon}$ is negative, and $t_{\mathrm{rel}}(P) - 1$ may also be negative or zero, so the left-hand side is not always a meaningful positive lower bound. The statement asserts only this single inequality ( $\le$ , not $<$ ), for every such $P$ , $\pi$ , and $\varepsilon$ .

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