Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

High-temperature fast mixing of Glauber dynamics

Proved
MarkovMixing.ising_high_temperature

by Shuze Chen · Aug 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmixing-timesprobability

Let GGG be a graph on nnn vertices with maximum degree Δ\DeltaΔ. The Ising model at inverse temperature β>0\beta>0β>0 puts spins ±1\pm1±1 on the vertices with Gibbs distribution π(σ)∝exp⁡(β∑{v,w}∈Eσ(v)σ(w))\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)\bigr)π(σ)∝exp(β∑{v,w}∈E​σ(v)σ(w)), 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 tmix(ε)t_{\mathrm{mix}}(\varepsilon)tmix​(ε) is the first ttt with max⁡σ∥Pt(σ,⋅)−π∥TV≤ε\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}\le\varepsilonmaxσ​∥Pt(σ,⋅)−π∥TV​≤ε, where ∥μ−ν∥TV=max⁡A∣μ(A)−ν(A)∣\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|∥μ−ν∥TV​=maxA​∣μ(A)−ν(A)∣ is the total variation distance.

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

  1. if Δtanh⁡β<1\Delta\tanh\beta<1Δtanhβ<1, then tmix(ε)≤⌈n(log⁡n+log⁡(1/ε))1−Δtanh⁡β⌉\displaystyle t_{\mathrm{mix}}(\varepsilon)\le\Bigl\lceil\frac{n\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\Delta\tanh\beta}\Bigr\rceiltmix​(ε)≤⌈1−Δtanhβn(logn+log(1/ε))​⌉;
  2. if every vertex of GGG has even degree and (Δ/2)tanh⁡(2β)<1(\Delta/2)\tanh(2\beta)<1(Δ/2)tanh(2β)<1, the same bound holds with 1−(Δ/2)tanh⁡(2β)1-(\Delta/2)\tanh(2\beta)1−(Δ/2)tanh(2β) in the denominator — a strictly weaker temperature condition.

At high temperature the Glauber dynamics mixes in order nlog⁡nn\log nnlogn 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⁡β<β\tanh\beta<\betatanhβ<β, condition 1 holds in particular whenever β<1/Δ\beta<1/\Deltaβ<1/Δ.

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

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me