High-temperature fast mixing of Glauber dynamics

Proved

MarkovMixing.ising_high_temperature

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$ . The Ising model at inverse temperature $\beta>0$ puts spins $\pm1$ on the vertices with Gibbs distribution $\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)\bigr)$ , and its Glauber dynamics picks a uniform vertex and re-samples its spin from $\pi$ conditioned on the other spins. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance.

The theorem (Theorem 15.1 of Levin–Peres–Wilmer, the capstone of Chapter 15) asserts, for every $0<\varepsilon<1$ :

if $\Delta\tanh\beta<1$ , then $\displaystyle t_{\mathrm{mix}}(\varepsilon)\le\Bigl\lceil\frac{n\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\Delta\tanh\beta}\Bigr\rceil$ ;
if every vertex of $G$ has even degree and $(\Delta/2)\tanh(2\beta)<1$ , the same bound holds with $1-(\Delta/2)\tanh(2\beta)$ in the denominator — a strictly weaker temperature condition.

At high temperature the Glauber dynamics mixes in order $n\log n$ steps on any graph — the fundamental fast-mixing criterion for spin systems. The proof is path coupling (Mission VIII) with the one-site coupling whose disagreement probability the tanh lemma controls; since $\tanh\beta<\beta$ , condition 1 holds in particular whenever $\beta<1/\Delta$ .

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 15.1** (LPW), the capstone of Chapter 15: fast mixing of the
Ising Glauber dynamics at high temperature.  On a graph with `n` vertices
and maximal degree `Δ`:
(i) if `Δ tanh β < 1`, then with `c(β) = 1 − Δ tanh β`,
`t_mix(ε) ≤ ⌈n(log n + log(1/ε))/c(β)⌉`;
(ii) if every vertex has even degree and `(Δ/2) tanh 2β < 1`, then the same
bound holds with `c_e(β) = 1 − (Δ/2) tanh 2β`. -/
theorem ising_high_temperature {Vv : Type*} [Fintype Vv] [DecidableEq Vv]
    [Nonempty Vv] (G : SimpleGraph Vv) [DecidableRel G.Adj]
    (β : ℝ) (hβ : 0 < β) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    ((G.maxDegree : ℝ) * Real.tanh β < 1 →
      (mixingTime (glauber (isingDist G β)) (isingDist G β) ε : ℝ) ≤
        ⌈(Fintype.card Vv : ℝ) *
            (Real.log (Fintype.card Vv) + Real.log (1 / ε)) /
          (1 - (G.maxDegree : ℝ) * Real.tanh β)⌉₊) ∧
    ((∀ v : Vv, Even (G.degree v)) →
      ((G.maxDegree : ℝ) / 2) * Real.tanh (2 * β) < 1 →
      (mixingTime (glauber (isingDist G β)) (isingDist G β) ε : ℝ) ≤
        ⌈(Fintype.card Vv : ℝ) *
            (Real.log (Fintype.card Vv) + Real.log (1 / ε)) /
          (1 - ((G.maxDegree : ℝ) / 2) * Real.tanh (2 * β))⌉₊) := 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 15.1, Theorem 15.1, Eqs. (15.1)-(15.2), pp. 201-202

Read-back

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

Read-back: ising_high_temperature

Setting. Let $V$ be a finite, nonempty type with decidable equality, $G$ a simple graph on $V$ with decidable adjacency, $\beta$ a real with $\beta > 0$ , and $\varepsilon$ a real with $0 < \varepsilon < 1$ . Write $n = |V|$ (the cardinality of the vertex type, not the number of configurations) and $\Delta$ for the maximum degree of $G$ (Mathlib's maxDegree, a natural number).

The objects involved, unfolded:

The Ising measure $\mu(\sigma)$ on configurations $\sigma : V \to \{\pm 1\}$ (encoded as functions to Bool, with spin $+1$ for true and $-1$ for false) is $w(\sigma) / \sum_\tau w(\tau)$ , where $w(\sigma) = \exp\big(\tfrac{\beta}{2}\sum_{v,w}[v\sim_G w]\, s_\sigma(v) s_\sigma(w)\big)$ ; the ordered double sum counts each edge twice, so the exponent is $\beta\sum_{\{v,w\}\in E(G)} s_\sigma(v)s_\sigma(w)$ .
The Glauber chain $P = \mathrm{glauber}(\mu)$ is the matrix on configurations with entry $P_{\sigma\tau} = \tfrac{1}{n}\sum_{v \in V} [\tau = \sigma \text{ off } v]\; \mu(\tau)\big/\sum_{\eta = \sigma \text{ off } v}\mu(\eta)$ : pick a uniformly random vertex $v$ and resample $\sigma(v)$ from $\mu$ conditioned on the other coordinates (with the total-division convention $x/0 = 0$ , immaterial here since $\mu > 0$ ).
The mixing time $t_{\mathrm{mix}}(\varepsilon) = \mathrm{mixingTime}(P, \mu, \varepsilon)$ is the natural number $\inf\{t \in \mathbb{N} : \sup_{\sigma} d_{TV}\big((P^t)_{\sigma,\cdot},\, \mu\big) \le \varepsilon\}$ , where $d_{TV}(\mu',\nu') = \sup_{A} \big|\sum_{x\in A}\mu'(x) - \sum_{x \in A}\nu'(x)\big|$ over all finite subsets $A$ of configurations, and the outer sup is over all starting configurations $\sigma$ . Junk convention: if no $t$ satisfies the condition, this $\inf$ over $\mathbb{N}$ is $0$ .
$\lceil r \rceil_+$ denotes the natural-number ceiling (Nat.ceil), which sends any negative real to $0$ .

The statement is a conjunction of two implications, both bounding the same quantity — the mixing time of the Glauber chain for $\mu$ , cast to a real:

Plain high-temperature bound. If

\Delta \cdot \tanh\beta \;<\; 1,

then

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Big\lceil \frac{n\big(\log n + \log(1/\varepsilon)\big)}{1 - \Delta\tanh\beta} \Big\rceil_+ .

Even-degree variant. If every vertex $v$ of $G$ has even degree (Mathlib's Even, which holds in particular for degree $0$ ) and

\frac{\Delta}{2}\cdot \tanh(2\beta) \;<\; 1,

then

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Big\lceil \frac{n\big(\log n + \log(1/\varepsilon)\big)}{1 - \tfrac{\Delta}{2}\tanh(2\beta)} \Big\rceil_+ .

In both parts the inequality compares the real cast of the natural-number mixing time against the natural-number ceiling of the real expression (also cast to a real); $\log$ is the real natural logarithm. Each implication is claimed only under its own high-temperature hypothesis; nothing is asserted when the respective hypothesis fails. Note that if $\mathbb{N}$ -infimum junk made the mixing time $0$ , or if $n = 1$ (so $\log n = 0$ ), the inequalities are simply as written — no separate case is carved out.

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