Section 3.2.1 -- the Metropolis chain for a symmetric base chain

Proved

MarkovMixing.metropolis_stationary

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

markov-chainsmixing-timesprobability

Let $\Psi$ be a symmetric stochastic matrix on a finite state space $V$ (a proposal chain with $\Psi(x,y)=\Psi(y,x)$ ), and let $\pi$ be a strictly positive probability distribution on $V$ . The Metropolis chain for this pair moves as follows: from the current state $x$ it proposes a state $y$ with probability $\Psi(x,y)$ , accepts the proposal with probability $\min\bigl(1,\pi(y)/\pi(x)\bigr)$ , and stays at $x$ if the proposal is rejected.

The theorem asserts three things about this chain: it is a genuine Markov chain (its transition matrix has nonnegative entries and rows summing to one); it satisfies the detailed balance equations $\pi(x)\,M(x,y)=\pi(y)\,M(y,x)$ for all states $x,y$ , i.e. it is reversible with respect to $\pi$ ; and $\pi$ is a stationary distribution for it, meaning $\sum_x \pi(x)\,M(x,y)=\pi(y)$ for every $y$ — running the chain one step from $\pi$ returns $\pi$ . This is the construction of §3.2.1 of Levin–Peres–Wilmer: a recipe turning any symmetric proposal mechanism into a chain with a prescribed stationary distribution.

Preamble

import Definitions.Def_mm_mcmc

Formal statement

namespace MarkovMixing

/-- **§3.2.1** (LPW): the Metropolis chain for a positive target distribution
`π` and a symmetric stochastic base chain `Ψ` is a Markov chain, reversible
with respect to `π`, with stationary distribution `π`. -/
theorem metropolis_stationary {V : Type*} [Fintype V] [DecidableEq V]
    (Ψ : Matrix V V ℝ) (hΨ : IsStochastic Ψ) (hsymm : ∀ x y : V, Ψ x y = Ψ y x)
    (π : V → ℝ) (hπ : IsDist π) (hpos : ∀ x : V, 0 < π x) :
    IsStochastic (metropolis Ψ π) ∧
    DetailedBalance (metropolis Ψ π) π ∧
    IsStationary (metropolis Ψ π) π := 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.2.1, pp. 37-39

Read-back

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

Let $V$ be an arbitrary finite type (with decidable equality); $V$ may be empty. Let $\Psi$ be a $V \times V$ matrix of real numbers which is stochastic in the sense that every entry satisfies $\Psi(x,y) \ge 0$ and every row sums to one, $\sum_y \Psi(x,y) = 1$ ; assume moreover that $\Psi$ is symmetric, $\Psi(x,y) = \Psi(y,x)$ for all $x, y \in V$ . Let $\pi : V \to \mathbb{R}$ be a function which is a distribution in the sense that $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ , and assume additionally that $\pi$ is strictly positive: $\pi(x) > 0$ for every $x \in V$ . Define the Metropolis matrix $M = \mathrm{metropolis}(\Psi, \pi)$ entrywise by

M(x,y) = \begin{cases} \Psi(x,y)\,\min\!\left(1, \dfrac{\pi(y)}{\pi(x)}\right) & \text{if } y \neq x,\\[2mm] 1 - \displaystyle\sum_{z \neq x} \Psi(x,z)\,\min\!\left(1, \dfrac{\pi(z)}{\pi(x)}\right) & \text{if } y = x, \end{cases}

where the sum in the diagonal case runs over all $z \in V$ with $z \neq x$ , and division is the (total) real division, which would return $0$ on division by zero — though here $\pi(x) > 0$ is assumed. The theorem asserts the conjunction of three claims about $M$ :

$M$ is stochastic: all entries of $M$ are $\ge 0$ and every row of $M$ sums to $1$ ;
$M$ satisfies detailed balance with respect to $\pi$ : for all $x, y \in V$ , $\pi(x)\, M(x,y) = \pi(y)\, M(y,x)$ ;
$\pi$ is stationary for $M$ , where this predicate bundles two things: $\pi$ is a distribution (nonnegative, summing to $1$ — restating a hypothesis already given), and the row vector $\pi$ multiplied on the left of $M$ equals $\pi$ , i.e. $\sum_x \pi(x)\, M(x,y) = \pi(y)$ for every $y \in V$ .

Note that if $V$ is empty, the hypotheses that rows of $\Psi$ sum to $1$ and that $\sum_x \pi(x) = 1$ are unsatisfiable ( $\emptyset$ -indexed sums are $0$ ), so in that degenerate case the statement holds vacuously.

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