Glauber dynamics on proper colorings mixes in $O(n\log n)$ for $q>2\Delta$

Proved

MarkovMixing.glauber_colorings_mixing

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

markov-chainsmixing-timesprobability

Let $G$ be a graph on $n$ vertices with maximum degree $\Delta$ , and fix a number of colors $q$ . A $q$ -coloring of the vertices is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color from the uniform distribution on the colorings that agree with the current one elsewhere — that is, uniformly among the colors legal at that vertex. Its stationary distribution is uniform over 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)|$ is the total variation distance.

The theorem (Theorem 14.8 of Levin–Peres–Wilmer, the capstone of Chapter 14) asserts: if $q>2\Delta$ , then for every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.

With a bit more than twice as many colors as the maximum degree, the dynamics mixes in order $n\log n$ steps. This is the flagship application of path coupling: colorings differing at one vertex are coupled by matching their proposed recolorings, and the single-edge contraction rate $(q-2\Delta)/\bigl(n(q-\Delta)\bigr)$ falls out of counting the disagreeing proposals.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 14.8** (LPW), the capstone of Chapter 14: for the Glauber
dynamics on proper `q`-colorings of a graph with `n` vertices and maximum
degree `Δ`, if `q > 2Δ`, then
`t_mix(ε) ≤ ⌈((q−Δ)/(q−2Δ)) n (log n − log ε)⌉`. -/
theorem glauber_colorings_mixing {Vv : Type*} [Fintype Vv] [DecidableEq Vv]
    [Nonempty Vv] (G : SimpleGraph Vv) [DecidableRel G.Adj] (q : ℕ)
    (hq : 2 * G.maxDegree < q) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (mixingTime (coloringGlauber G q)
        (uniformDist {c : Vv → Fin q // IsProperColoring G c}) ε : ℝ) ≤
      ⌈((q : ℝ) - G.maxDegree) / ((q : ℝ) - 2 * G.maxDegree) *
        (Fintype.card Vv) *
        (Real.log (Fintype.card Vv) - Real.log ε)⌉₊ := 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 14.3, Theorem 14.8, Eq. (14.17), p. 193

Read-back

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

Read-back: glauber_colorings_mixing

Let $Vv$ be a finite, nonempty type with decidable equality, $G$ a simple graph on $Vv$ with decidable adjacency, and $q$ a natural number satisfying $2\Delta < q$ , where $\Delta$ denotes $G$ 's maximum vertex degree. Let $\varepsilon$ be a real number with $0 < \varepsilon < 1$ . Write $n = |Vv|$ and let $\Omega$ be the set of proper $q$ -colorings of $G$ — maps $c : Vv \to \{0,\dots,q-1\}$ with $c(v) \ne c(w)$ for every adjacent pair $v \sim w$ — and $N = |\Omega|$ .

The Markov chain in question is the matrix $M$ indexed by $\Omega$ obtained by restricting to proper colorings the Glauber matrix for the weight $\pi$ that assigns $1/N$ to each proper coloring and $0$ to each improper one. Concretely, for proper colorings $x, y$ ,

M(x,y) \;=\; \frac{1}{n} \sum_{v \in Vv} \begin{cases} \dfrac{\pi(y)}{\sum_{z : z \equiv x \text{ off } v} \pi(z)} & \text{if } y \text{ agrees with } x \text{ at every vertex} \ne v,\\[1.5ex] 0 & \text{otherwise,} \end{cases}

the denominator summing $\pi$ over all colorings $z$ (proper or not) that agree with $x$ away from $v$ — i.e., pick a uniformly random vertex and resample its color proportionally to the uniform-on-proper weight among colorings differing only there (Lean's total division makes a zero-denominator summand equal to $0$ ; the rows of $M$ are copied from the full-space Glauber matrix without renormalization after restriction).

The theorem asserts a single inequality:

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Big\lceil \frac{q - \Delta}{\,q - 2\Delta\,}\; n\; \big(\log n - \log \varepsilon\big) \Big\rceil_{\!+},

where the left side (cast from $\mathbb{N}$ to $\mathbb{R}$ ) is the least natural $t$ such that

\sup_{x \in \Omega}\; \sup_{A \subseteq \Omega} \Big| \sum_{c \in A} M^t(x,c) - \sum_{c \in A} \tfrac{1}{N} \Big| \;\le\; \varepsilon,

i.e. the mixing time of $M$ to the uniform distribution on $\Omega$ (constant $1/N$ , with $(0:\mathbb{R})^{-1} = 0$ if $N = 0$ ) under the total-variation-style distance without a factor $\tfrac12$ ; and $\lceil\cdot\rceil_+$ is the ceiling into $\mathbb{N}$ , clamping negative reals to $0$ . In the bound, $q$ , $\Delta$ , and $n$ are natural numbers cast to $\mathbb{R}$ , the subtractions $q - \Delta$ and $q - 2\Delta$ are real subtractions (no truncation; both are positive under $2\Delta < q$ ), and $\log$ is the real logarithm ( $\log \varepsilon < 0$ for $\varepsilon < 1$ ; $\log n = 0$ when $n = 1$ ).

Junk/edge behavior the statement's meaning rests on: the mixing time is a natural-number infimum that equals $0$ if no time achieves distance $\le \varepsilon$ ; if $\Omega$ is empty ( $N = 0$ ), the suprema over the empty index type $\Omega$ are $0 \le \varepsilon$ , so the mixing time is $0$ and the inequality trivializes. Nothing in the statement asserts that $M$ is stochastic, irreducible, or that the uniform distribution is stationary for it — only the mixing-time inequality is claimed.

Human review

Endorsed by Community (Bot) · Aug 22, 2026
Endorsed by Shuze Chen · Aug 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Glauber dynamics on proper colorings mixes in O(nlog⁡n)O(n\log n)O(nlogn) for q>2Δq>2\Deltaq>2Δ

Read-back: glauber_colorings_mixing

Glauber dynamics on proper colorings mixes in $O(n\log n)$ for $q>2\Delta$