Section 3.3.2 -- stationarity of the Glauber dynamics

Proved

MarkovMixing.glauber_stationary

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

markov-chainsmixing-timesprobability

Let $\pi$ be a probability distribution on the space of configurations $x:\mathcal V\to S$ , which assign a spin from a finite set $S$ to each site of a finite nonempty set $\mathcal V$ . The Glauber dynamics (single-site heat bath) for $\pi$ makes one step as follows: pick a site $v$ uniformly at random, and replace the spin at $v$ by a sample from $\pi$ conditioned on agreeing with the current configuration at every site other than $v$ .

The theorem asserts four things about the resulting transition matrix $G$ . First, all entries are nonnegative. Second, for every configuration $x$ in the support of $\pi$ (i.e. with $\pi(x)>0$ ) the row of $G$ at $x$ sums to one — so restricted to the support, $G$ is a genuine Markov chain. (Positivity of $\pi$ is not assumed, and at a configuration of zero mass the conditioning that defines a step can be vacuous, so row sums are claimed only on the support.) Third, $G$ satisfies the detailed balance equations $\pi(x)\,G(x,y)=\pi(y)\,G(y,x)$ for all configurations $x,y$ — reversibility with respect to $\pi$ . Fourth, $\pi$ is a stationary distribution: $\sum_x\pi(x)\,G(x,y)=\pi(y)$ for every $y$ . This is Exercise 3.2 (§3.3.2) of Levin–Peres–Wilmer.

Preamble

import Definitions.Def_mm_mcmc

Formal statement

namespace MarkovMixing

/-- **§3.3.2, Exercise 3.2** (LPW): the Glauber dynamics for a distribution
`π` on configurations is reversible with respect to `π` and has stationary
distribution `π`; its entries are nonnegative and every row at a
configuration in the support of `π` sums to `1`. -/
theorem glauber_stationary {Vv S : Type*} [Fintype Vv] [DecidableEq Vv]
    [Fintype S] [DecidableEq S] [Nonempty Vv]
    (π : (Vv → S) → ℝ) (hπ : IsDist π) :
    (∀ x y : Vv → S, 0 ≤ glauber π x y) ∧
    (∀ x : Vv → S, 0 < π x → ∑ y, glauber π x y = 1) ∧
    DetailedBalance (glauber π) π ∧
    IsStationary (glauber π) π := 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 3.3.2, Eq. (3.6) and Exercise 3.2, pp. 41-42

Read-back

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

Let $V$ be a finite nonempty type of "sites" and $S$ a finite type of "spins" (both with decidable equality; $S$ is allowed to be empty, in which case the configuration space below is empty and the distribution hypothesis becomes unsatisfiable). The state space is the set of configurations $\Omega = S^V$ , i.e. functions $x : V \to S$ . Let $\pi : \Omega \to \mathbb{R}$ be a distribution: $\pi(x) \ge 0$ for every configuration $x$ , and $\sum_{x \in \Omega} \pi(x) = 1$ . Note that strict positivity of $\pi$ is not assumed. Define the Glauber (heat-bath) matrix $G = \mathrm{glauber}(\pi)$ on $\Omega \times \Omega$ by

G(x,y) = \frac{1}{|V|} \sum_{v \in V} \begin{cases} \dfrac{\pi(y)}{\displaystyle\sum_{z \,:\, z(w) = x(w)\ \forall w \neq v} \pi(z)} & \text{if } y(w) = x(w) \text{ for all } w \neq v,\\[3mm] 0 & \text{otherwise,} \end{cases}

that is: average over the sites $v$ ; the summand for site $v$ is nonzero only when $y$ agrees with $x$ everywhere except possibly at $v$ , in which case it equals $\pi(y)$ divided by the total $\pi$ -mass of all configurations agreeing with $x$ off $v$ . Division is the total real division returning $0$ when the denominator is $0$ (so a site whose conditional mass vanishes contributes $0$ ). When $y = x$ , the agreement condition holds for every site $v$ , so every term of the average contributes. The theorem asserts the conjunction of four claims:

Nonnegativity of all entries: $G(x,y) \ge 0$ for all configurations $x, y$ ;
Conditional row sums: for every configuration $x$ with $\pi(x) > 0$ , the row of $G$ at $x$ sums to one, $\sum_y G(x,y) = 1$ . (Nothing is claimed about the row sums at configurations $x$ with $\pi(x) = 0$ ; in particular, full stochasticity of $G$ is not claimed.)
Detailed balance: for all configurations $x, y$ , $\pi(x)\, G(x,y) = \pi(y)\, G(y,x)$ ;
Stationarity: the predicate bundles two parts — $\pi$ is a distribution (nonnegative, summing to $1$ ; a restatement of the hypothesis), and the row vector $\pi$ is fixed under right-multiplication by $G$ : $\sum_x \pi(x)\, G(x,y) = \pi(y)$ for every configuration $y$ . This last identity is claimed for all $y$ , with no positivity restriction.

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