Section 3.2.2 -- the Metropolis-Hastings chain for a general base chain

Proved

MarkovMixing.metropolized_stationary

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

markov-chainsmixing-timesprobability

Let $\Psi$ be an arbitrary stochastic matrix on a finite state space $V$ (a base chain, not assumed symmetric), and let $\pi$ be a strictly positive probability distribution on $V$ . The Metropolis–Hastings chain built from this pair proposes a move from $x$ to $y$ with probability $\Psi(x,y)$ and accepts it with probability

\min\!\Bigl(1,\;\frac{\pi(y)\,\Psi(y,x)}{\pi(x)\,\Psi(x,y)}\Bigr),

staying at $x$ on rejection; the acceptance ratio weighs the proposal probabilities of the two directions against the target masses.

The theorem asserts that this chain is a genuine Markov chain (nonnegative entries, rows summing to one), that it satisfies the detailed balance equations $\pi(x)\,M(x,y)=\pi(y)\,M(y,x)$ — reversibility with respect to $\pi$ — and that $\pi$ is a stationary distribution for it: $\sum_x\pi(x)\,M(x,y)=\pi(y)$ for every $y$ . This is Exercise 3.1 of Levin–Peres–Wilmer, the general (non-symmetric) form of the Metropolis construction of §3.2.2.

Preamble

import Definitions.Def_mm_mcmc

Formal statement

namespace MarkovMixing

/-- **§3.2.2, Exercise 3.1** (LPW): the Metropolized chain built from a
general stochastic base chain `Ψ` and a positive target distribution `π` is a
Markov chain, reversible with respect to `π`, with stationary distribution
`π`. -/
theorem metropolized_stationary {V : Type*} [Fintype V] [DecidableEq V]
    (Ψ : Matrix V V ℝ) (hΨ : IsStochastic Ψ)
    (π : V → ℝ) (hπ : IsDist π) (hpos : ∀ x : V, 0 < π x) :
    IsStochastic (metropolized Ψ π) ∧
    DetailedBalance (metropolized Ψ π) π ∧
    IsStationary (metropolized Ψ π) π := 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.2, Eq. (3.5) and Exercise 3.1, p. 40

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$ real matrix which is stochastic: every entry satisfies $\Psi(x,y) \ge 0$ and every row sums to one, $\sum_y \Psi(x,y) = 1$ . No symmetry or irreducibility is assumed of $\Psi$ . Let $\pi : V \to \mathbb{R}$ be a distribution ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ) which is moreover strictly positive: $\pi(x) > 0$ for every $x \in V$ . Define the Metropolis–Hastings ("metropolized") matrix $M = \mathrm{metropolized}(\Psi, \pi)$ entrywise by

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

where the diagonal sum runs over all $z \in V$ with $z \neq x$ . Division here is the total real division that returns $0$ when the denominator is $0$ : in particular, if $\Psi(x,y) = 0$ (with $y \neq x$ ), the acceptance ratio is $\min(1, 0) = 0$ by this convention, and the corresponding entry is $0 \cdot 0 = 0$ . The theorem asserts the conjunction of three claims about $M$ :

$M$ is stochastic: $M(x,y) \ge 0$ for all $x, y \in V$ , and $\sum_y M(x,y) = 1$ for every $x \in V$ ;
$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$ , a predicate bundling two parts: $\pi$ is a distribution (nonnegative and summing to $1$ , restating a hypothesis already assumed), and the row vector $\pi$ is fixed by right-multiplication by $M$ , i.e. $\sum_x \pi(x)\, M(x,y) = \pi(y)$ for every $y \in V$ .

If $V$ is empty, the hypotheses that the rows of $\Psi$ sum to $1$ and that $\sum_x \pi(x) = 1$ cannot hold (empty sums are $0$ ), so the statement is vacuously true in that case.

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