Curie--Weiss: fast mixing for $\alpha<1$

Proved

MarkovMixing.ising_complete_graph_fast

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

markov-chainsmixing-timesprobability

The Curie–Weiss model is the Ising model on the complete graph $K_n$ : spins $\pm1$ on $n$ vertices, every pair interacting, with Gibbs distribution $\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}}\sigma(v)\sigma(w)\bigr)$ at inverse temperature $\beta=\alpha/n$ — the $1/n$ scaling that makes the total interaction per site of constant order, with $\alpha$ the effective temperature parameter. The Glauber dynamics re-samples a uniformly chosen site from the conditional distribution; 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)|$ .

The theorem (Theorem 15.3(i) of Levin–Peres–Wilmer) asserts: for every $n\ge2$ , every $0<\alpha<1$ , and every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{n\,\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\alpha}\Bigr\rceil.

Below the critical value $\alpha=1$ the mean-field dynamics mixes in order $n\log n$ steps. The proof is one line from the high-temperature theorem of this mission: on $K_n$ the degree is $n-1$ and $(n-1)\tanh(\alpha/n)\le\alpha$ . The companion theorem shows that above $\alpha=1$ the same dynamics needs exponentially many steps — the dynamical phase transition.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 15.3(i)** (LPW): for the Glauber dynamics of the Ising model
on the complete graph on `n` vertices at `β = α/n` with `α < 1`,
`t_mix(ε) ≤ ⌈n(log n + log(1/ε))/(1−α)⌉` (the ceiling absorbs integer
rounding). -/
theorem ising_complete_graph_fast (n : ℕ) (hn : 2 ≤ n)
    (α : ℝ) (hα0 : 0 < α) (hα : α < 1) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (mixingTime (glauber (isingDist (⊤ : SimpleGraph (Fin n)) (α / n)))
        (isingDist (⊤ : SimpleGraph (Fin n)) (α / n)) ε : ℝ) ≤
      ⌈(n : ℝ) * (Real.log n + Real.log (1 / ε)) / (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 15.2, Theorem 15.3(i), Eq. (15.8), p. 203

Read-back

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

Read-back: `ising_complete_graph_fast`

Let $n \in \mathbb{N}$ with $n \ge 2$ , let $\alpha$ be a real number with $0 < \alpha < 1$ , and let $\varepsilon$ be a real number with $0 < \varepsilon < 1$ . The state space is the set of spin configurations $\sigma : \{0,\dots,n-1\} \to \{\mathrm{true},\mathrm{false}\}$ ( $2^n$ states). Write $s_\sigma(v) = +1$ if $\sigma(v) = \mathrm{true}$ and $-1$ otherwise.

The measure. $\mu$ is the Ising distribution on the complete graph $K_n$ (the top simple graph on $n$ vertices, whose adjacency is exactly $v \ne w$ ) at parameter $\beta = \alpha/n$ :

\mu(\sigma) \;=\; \frac{w(\sigma)}{\sum_{\tau} w(\tau)}, \qquad w(\sigma) \;=\; \exp\!\Bigl( \frac{\alpha}{n} \cdot \frac12 \sum_{v} \sum_{w \,:\, w \ne v} s_\sigma(v)\, s_\sigma(w) \Bigr),

where the double sum ranges over all ordered pairs of distinct vertices (each unordered pair counted twice, so the exponent equals $\frac{\alpha}{n} \sum_{\{v,w\}} s_\sigma(v) s_\sigma(w)$ over unordered pairs). The division defining $\mu$ is total real division, but the denominator is a sum of $2^n$ strictly positive exponentials, so no division-by-zero junk arises here.

The chain. $P$ is the Glauber (single-site heat-bath) dynamics associated with $\mu$ : for configurations $x, y$ ,

P(x,y) \;=\; \frac{1}{n} \sum_{v=0}^{n-1} \begin{cases} \dfrac{\mu(y)}{\displaystyle\sum_{z \,:\, z \equiv x \text{ off } v} \mu(z)} & \text{if } y \text{ agrees with } x \text{ at every site} \ne v, \\[2pt] 0 & \text{otherwise,} \end{cases}

where " $z \equiv x$ off $v$ " means $z(w) = x(w)$ for all $w \ne v$ (so the inner sum has exactly two terms, the two choices of value at $v$ ). If $y$ differs from $x$ at two or more sites, every summand is $0$ ; if $y$ differs from $x$ at exactly one site $v$ , only that $v$ contributes; if $y = x$ , all $n$ sites contribute. The inner division is again total but its denominator is positive.

The claim. With the mixing distance measured against this same $\mu$ ,

d(t) \;=\; \sup_{x}\; \sup_{A} \Bigl| \sum_{y \in A} (P^{t})(x,y) \;-\; \sum_{y \in A} \mu(y) \Bigr|,

the suprema running over all $2^n$ starting configurations $x$ and all subsets $A$ of the (finite) configuration space, and with $t_{\mathrm{mix}}(\varepsilon)$ the least natural number $t$ such that $d(t) \le \varepsilon$ (the infimum of the empty set of naturals being the junk value $0$ if no such $t$ existed), the theorem asserts

\bigl(t_{\mathrm{mix}}(\varepsilon) : \mathbb{R}\bigr) \;\le\; \Bigl\lceil \frac{n \left( \log n + \log(1/\varepsilon) \right)}{1 - \alpha} \Bigr\rceil_{\mathbb{N}},

where $\log$ is the real natural logarithm and $\lceil \cdot \rceil_{\mathbb{N}}$ is the natural-number ceiling, which sends every nonpositive real to $0$ (under the given hypotheses $n \ge 2$ , $\varepsilon < 1$ , $\alpha < 1$ , the argument $n(\log n + \log(1/\varepsilon))/(1-\alpha)$ is strictly positive, so no clamping occurs). The left-hand side is the mixing time, a natural number, cast to $\mathbb{R}$ .

Nothing else is hypothesized or asserted: in particular the statement does not include any assumption that $\mu$ is stationary for $P$ — the distribution $\mu$ simply appears both as the input to the Glauber construction and as the reference measure inside the mixing-time definition.

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

Curie--Weiss: fast mixing for α<1\alpha<1α<1

Read-back: ising_complete_graph_fast

Curie--Weiss: fast mixing for $\alpha<1$

Read-back: `ising_complete_graph_fast`