Theorem 5.7 -- fast mixing of the Metropolis chain on colorings

Proved

MarkovMixing.colorings_mixing

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

markov-chainsmixing-timesprobability

Let $G$ be a graph on $n$ vertices with maximal degree $\Delta$ , and fix a number of colors $q$ . A $q$ -coloring of the vertices is proper if adjacent vertices always receive distinct colors. The Metropolis chain on proper colorings moves as follows: pick a vertex $v$ and a color $k$ uniformly at random, recolor $v$ with $k$ if the result is again a proper coloring, and do nothing otherwise. Its stationary distribution is uniform on the proper colorings. 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 5.7 of Levin–Peres–Wilmer) asserts: if $q>3\Delta$ — enough colors relative to the degree — then for every $0<\varepsilon\le1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl(1-\frac{3\Delta}{q}\Bigr)^{-1} n\,\bigl(\log n+\log\varepsilon^{-1}\bigr)\;+\;1.

So with $q>3\Delta$ colors the chain mixes in order $n\log n$ steps. (The trailing $+1$ absorbs the rounding of the real-valued bound to an integer time.)

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 5.7** (LPW): for the Metropolis chain on proper `q`-colorings
of a graph with `n` vertices and maximal degree `Δ`, if `q > 3Δ`, then with
`c_met(Δ,q) = 1 − 3Δ/q`,
`t_mix(ε) ≤ c_met(Δ,q)⁻¹ n (log n + log(1/ε)) + 1`. -/
theorem colorings_mixing {Vv : Type*} [Fintype Vv] [DecidableEq Vv] [Nonempty Vv]
    (G : SimpleGraph Vv) [DecidableRel G.Adj] (q : ℕ)
    (hq : 3 * G.maxDegree < q) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) :
    (mixingTime (coloringMetropolis G q)
        (uniformDist {c : Vv → Fin q // IsProperColoring G c}) ε : ℝ) ≤
      (1 - 3 * (G.maxDegree : ℝ) / q)⁻¹ * (Fintype.card Vv) *
        (Real.log (Fintype.card Vv) + Real.log ε⁻¹) + 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 5.4.1, Theorem 5.7, p. 70

Read-back

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

Let $\mathcal{V}$ be a finite, nonempty vertex type with decidable equality, $G$ a simple graph on $\mathcal{V}$ with decidable adjacency, and $q$ a natural number of colors satisfying the strict hypothesis $3\Delta < q$ , where $\Delta$ is the maximum vertex degree of $G$ (this forces $q \ge 1$ ). Let $\varepsilon$ be a real number with $0 < \varepsilon \le 1$ . The state space is the set $\Omega$ of proper $q$ -colorings of $G$ : functions $c : \mathcal{V} \to \{0,\dots,q-1\}$ such that $c(v) \ne c(w)$ whenever $v \sim w$ in $G$ . On $\Omega$ the theorem considers the following specific Markov chain $P$ (a real $\Omega \times \Omega$ matrix): for two distinct proper colorings $x \ne y$ , the transition probability is

P(x,y) \;=\; \begin{cases} \dfrac{1}{|\mathcal{V}| \cdot q} & \text{if } x \text{ and } y \text{ differ at exactly one vertex},\\[4pt] 0 & \text{otherwise,} \end{cases}

and the diagonal entry is defined as the complement $P(x,x) = 1 - \sum_{z \ne x} P(x,z)$ , so each row sums to $1$ by construction (the definition does not itself assert that $P(x,x) \ge 0$ ; that is a consequence, not a hypothesis). This is the chain that proposes a uniformly random vertex and a uniformly random one of the $q$ colors — each of the $|\mathcal{V}|\, q$ proposals having probability $1/(|\mathcal{V}| q)$ — and accepts exactly when the modified coloring is again proper (proposals recoloring a vertex with its current color, or producing an improper coloring, contribute to holding in place). The target distribution is the uniform distribution $u$ on $\Omega$ , assigning every proper coloring the mass $1/|\Omega|$ ; note that if $G$ had no proper $q$ -coloring then $\Omega$ would be empty and, by the total-function convention $1/0 = 0$ , $u$ would be identically zero — the statement itself does not assume $\Omega$ is nonempty. With total-variation distance $\mathrm{d_{TV}}(\mu,\nu) = \sup_{A \subseteq \Omega} \big|\sum_{x\in A}\mu(x) - \sum_{x\in A}\nu(x)\big|$ and worst-case distance $d(t) = \sup_{x \in \Omega} \mathrm{d_{TV}}\big(P^t(x,\cdot),\, u\big)$ (row $x$ of the $t$ -th power of $P$ ), the mixing time is

t_{\mathrm{mix}}(\varepsilon) \;=\; \inf\{\, t \in \mathbb{N} : d(t) \le \varepsilon \,\},

with the convention that the infimum of an empty set of naturals is $0$ , so the left side would be $0$ (and the claim vacuously easy) if no time ever brought the chain within $\varepsilon$ of $u$ . The theorem asserts the single inequality, with the natural number $t_{\mathrm{mix}}(\varepsilon)$ cast to a real:

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Big(1 - \frac{3\Delta}{q}\Big)^{-1} \cdot |\mathcal{V}| \cdot \Big(\ln |\mathcal{V}| + \ln \varepsilon^{-1}\Big) \;+\; 1,

where $\Delta$ and $q$ are cast to reals (the hypothesis $3\Delta < q$ makes $1 - 3\Delta/q$ strictly positive, so the inverse is genuine), $\ln$ is the natural logarithm (not base $2$ ), $\ln|\mathcal{V}| \ge 0$ since $\mathcal{V}$ is nonempty, and $\ln \varepsilon^{-1} \ge 0$ since $\varepsilon \le 1$ . The bound is stated for this one fixed graph, color count, and $\varepsilon$ (all universally quantified); nothing is claimed about lower bounds, about the chain's irreducibility or stationarity of $u$ , or for $q \le 3\Delta$ .

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