The maximal Metropolis–Hastings kernel satisfies detailed balance

Proved

TierneyMH.Mixture.maxMHKernel_reversible

by mikedeng1 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chain-monte-carlomarkov-kernelmetropolis-hastingsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\pi$ be a probability measure and $Q$ a Markov proposal kernel on a measurable space $(E,\mathcal E)$ . The maximal Metropolis–Hastings kernel $P$ for $Q$ , the kernel (1) with acceptance probability $\alpha_{MH}$ , satisfies the detailed balance relation

\pi(dx)\,P(x,dy)=\pi(dy)\,P(y,dx)

as measures on $\mathcal E\otimes\mathcal E$ . In particular $\pi$ is invariant for $P$ .

In the paper this follows from the fact that $\alpha_{MH}$ satisfies conditions (i) and (ii) together with Theorem 2. It is what makes the off-diagonal ordering of Proposition 5 a comparison between kernels with invariant distribution $\pi$ , as the definition of $\succeq$ presupposes.

Formalization Note Detailed balance is Mathlib's Kernel.IsReversible: $\int_A P(x,B)\,\pi(dx)=\int_B P(x,A)\,\pi(dx)$ for all measurable $A,B$ .

Preamble

import Mathlib
import Definitions.Def_TierneyMH_Mixture_maxMHKernel

open MeasureTheory ProbabilityTheory
open scoped ENNReal

Formal statement

namespace TierneyMH.Mixture

/-- **The maximal Metropolis–Hastings kernel is reversible** (Tierney 1998, §2, p. 3:
`α_MH` satisfies (i)–(ii), so by Theorem 2 the kernel satisfies detailed balance).
For a probability measure `π` and a Markov proposal kernel `Q`, the kernel (1) with
acceptance probability `α_MH` satisfies the detailed balance relation (2),
`π(dx) P(x, dy) = π(dy) P(y, dx)`. -/
theorem maxMHKernel_reversible {E : Type*} [MeasurableSpace E]
    (π : Measure E) [IsProbabilityMeasure π] (Q : Kernel E E) [IsMarkovKernel Q] :
    Kernel.IsReversible (maxMHKernel π Q) π := by sorry

end TierneyMH.Mixture

Source

L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, Ann. Appl. Probab. 8(1) (1998) 1–9, DOI 10.1214/aoap/1027961031, p. 3, §2 (α_MH satisfies (i)–(ii); by Theorem 2 the maximal kernel is reversible)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph