Theorem 5.8 -- fast mixing of the hardcore Glauber dynamics

Proved

MarkovMixing.hardcore_glauber_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 maximum degree $\Delta$ . A $\{0,1\}$ -configuration on the vertices is hardcore if no two adjacent vertices are both occupied — the occupied sites form an independent set. The hardcore model with fugacity $\lambda>0$ is the distribution on hardcore configurations with $\pi(\sigma)\propto\lambda^{|\sigma|}$ , where $|\sigma|$ is the number of occupied sites. The Glauber dynamics for $\pi$ picks a uniform vertex and re-samples its occupancy from $\pi$ conditioned on the rest of the configuration; here it is viewed as a chain on the hardcore configurations. 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.8 of Levin–Peres–Wilmer) asserts: if $\lambda(\Delta-1)<1$ , then for every $0<\varepsilon\le1$ ,

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

Below the threshold $\lambda<(\Delta-1)^{-1}$ the dynamics mixes in order $n\log n$ steps. (The $+1$ absorbs integer rounding.)

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 5.8** (LPW): for the Glauber dynamics of the hardcore model
with fugacity `λ` on a graph with `n` vertices and maximum degree `Δ`, if
`λ < (Δ − 1)⁻¹`, then with `c_H(λ) = (1 + λ(1 − Δ))/(1 + λ)`,
`t_mix(ε) ≤ (n / c_H(λ)) (log n + log(1/ε)) + 1`. -/
theorem hardcore_glauber_mixing {Vv : Type*} [Fintype Vv] [DecidableEq Vv]
    [Nonempty Vv] (G : SimpleGraph Vv) [DecidableRel G.Adj]
    (lam : ℝ) (hlam : 0 < lam) (hc : lam * ((G.maxDegree : ℝ) - 1) < 1)
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) :
    (mixingTime
        (subChain (glauber (hardcoreDist G lam)) (IsHardcore G))
        (fun σ : {σ : Vv → Bool // IsHardcore G σ} => hardcoreDist G lam σ.1)
        ε : ℝ) ≤
      ((Fintype.card Vv : ℝ) * (1 + lam) / (1 + lam * (1 - (G.maxDegree : ℝ)))) *
        (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.2, Theorem 5.8, pp. 70-71

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, $\lambda$ a real number with $\lambda > 0$ , and assume the hypothesis

\lambda \cdot (\Delta - 1) \;<\; 1,

where $\Delta$ is the maximum vertex degree of $G$ cast to a real and the subtraction is real subtraction — so for $\Delta = 0$ this reads $-\lambda < 1$ and holds automatically, and for $\Delta \ge 2$ it is exactly $\lambda < 1/(\Delta - 1)$ . Let $\varepsilon$ be real with $0 < \varepsilon \le 1$ . A Boolean configuration $\sigma : \mathcal{V} \to \{\mathrm{false},\mathrm{true}\}$ is hard-core admissible when no edge of $G$ has both endpoints set to true (i.e. the true-set of $\sigma$ is an independent set). The hard-core distribution $\mu$ on all Boolean configurations is defined by $\mu(\sigma) = w(\sigma)/Z$ where $w(\sigma) = \lambda^{|\{v : \sigma(v) = \mathrm{true}\}|}$ if $\sigma$ is admissible and $w(\sigma) = 0$ otherwise, and $Z = \sum_{\tau} w(\tau)$ , the sum over all Boolean configurations (which equals the sum over admissible ones). The Glauber dynamics for $\mu$ is the matrix on the full configuration space $\mathcal{V} \to \{\mathrm{false},\mathrm{true}\}$ given by

P(x, y) \;=\; \frac{1}{|\mathcal{V}|} \sum_{v \in \mathcal{V}} \mathbf{1}\big[\, y(w) = x(w) \text{ for all } w \ne v \,\big] \cdot \frac{\mu(y)}{\sum_{z :\, z(w) = x(w)\ \forall w \ne v} \mu(z)},

i.e. pick a uniformly random vertex $v$ and resample the value at $v$ from $\mu$ conditioned on the other coordinates (when $y = x$ , the indicator holds for every $v$ , so the diagonal entry accumulates all $|\mathcal{V}|$ terms; divisions here are the total-function convention, with $r/0 = 0$ if a conditional normalizer were zero). The chain in the theorem is the restriction of this matrix to the subtype of admissible configurations: states are pairs $\sigma$ ranging over admissible configurations only, with entries simply inherited from $P$ (the restriction is taken entrywise; the statement does not itself assert that the restricted rows sum to $1$ ). The target distribution on this subtype assigns to an admissible $\sigma$ the value $\mu(\sigma) = \lambda^{|\sigma|}/Z$ as above. Writing $\mathrm{d_{TV}}(\alpha,\beta) = \sup_{A} |\sum_{x \in A} \alpha(x) - \sum_{x \in A} \beta(x)|$ (supremum over subsets of the admissible configurations), $d(t) = \sup_{x} \mathrm{d_{TV}}\big(P_{\mathrm{res}}^t(x, \cdot),\, \mu\big)$ with the supremum over admissible starting states and $P_{\mathrm{res}}^t$ the $t$ -th power of the restricted matrix, 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 is $0$ , and the claim trivial, if no time ever achieves distance $\le \varepsilon$ ). The theorem asserts the single inequality, with $t_{\mathrm{mix}}(\varepsilon)$ cast to a real:

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

where $|\mathcal{V}|$ is the number of vertices cast to a real, the denominator $1 + \lambda(1 - \Delta) = 1 - \lambda(\Delta - 1)$ is strictly positive by the hypothesis, and $\ln$ is the natural logarithm ( $\ln|\mathcal{V}| \ge 0$ since $\mathcal{V}$ is nonempty, and $\ln \varepsilon^{-1} \ge 0$ since $\varepsilon \le 1$ ). Nothing else is asserted: no lower bound, no claim that $\mu$ is stationary for the restricted chain or that the restricted chain is stochastic, and the bound is for the one graph, fugacity $\lambda$ , and accuracy $\varepsilon$ quantified 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