Prove2Me

π(dx)Q(x,dy)αMH(x,y)=min⁡{h(y,x),h(x,y)} ν(dx,dy)\pi(dx)Q(x,dy)\alpha_{MH}(x,y)=\min\{h(y,x),h(x,y)\}\,\nu(dx,dy) for any symmetric dominating ν\nu

Proved
TierneyMH.Mixture.alphaMH_density_form

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 QQ a Markov proposal kernel on EE, and let μ(dx,dy)=π(dx)Q(x,dy)\mu(dx,dy)=\pi(dx)Q(x,dy). Let ν\nu be any σ\sigma-finite measure on E×EE\times E that is symmetric, ν(dx,dy)=ν(dy,dx)\nu(dx,dy)=\nu(dy,dx), and dominates μ\mu, and let h=dμ/dνh=d\mu/d\nu. Then, as measures on E×EE\times E,

π(dx) Q(x,dy) αMH(x,y)=min⁡{h(y,x), h(x,y)} ν(dx,dy).\pi(dx)\,Q(x,dy)\,\alpha_{MH}(x,y) = \min\{h(y,x),\,h(x,y)\}\,\nu(dx,dy).

This is the first step of the proof of Proposition 5, where it is applied to the mixture proposal: the part of the joint law of a move that is accepted has density min⁡{h(y,x),h(x,y)}\min\{h(y,x),h(x,y)\} with respect to every symmetric dominating measure, not only the one used to define αMH\alpha_{MH}.

Formalization Note The page writes the first equality as h(x,y)min⁡{h(y,x)/h(x,y),1} ν(dx,dy)h(x,y)\min\{h(y,x)/h(x,y),1\}\,\nu(dx,dy) for the mixture Q=∑iβiQiQ=\sum_i\beta_iQ_i; the statement gives the resulting min form, for an arbitrary Markov proposal kernel. αMH\alpha_{MH} is defined through the specific measure μ+μT\mu+\mu^T; the theorem relates it to an arbitrary symmetric dominating ν\nu.

Preamble
import Mathlib
import Definitions.Def_TierneyMH_Mixture_alphaMH

open MeasureTheory ProbabilityTheory
open scoped ENNReal
Formal statement
namespace TierneyMH.Mixture

/-- **Density form of `μ α_MH`** (Tierney 1998, proof of Proposition 5, p. 8, first two lines
of the display). Let `ν` be any σ-finite symmetric measure on `E × E` (`ν(dx, dy) = ν(dy, dx)`)
dominating `μ(dx, dy) = π(dx) Q(x, dy)`, and let `h = dμ/dν`. Then
`π(dx) Q(x, dy) α_MH(x, y) = min{h(y, x), h(x, y)} ν(dx, dy)`
as measures on `E × E`. -/
theorem alphaMH_density_form {E : Type*} [MeasurableSpace E]
    (π : Measure E) [IsProbabilityMeasure π] (Q : Kernel E E) [IsMarkovKernel Q]
    (ν : Measure (E × E)) [SigmaFinite ν] (hν_symm : ν.map Prod.swap = ν)
    (hμν : π ⊗ₘ Q ≪ ν) :
    (π ⊗ₘ Q).withDensity (alphaMH π Q) =
      ν.withDensity (fun p => min ((π ⊗ₘ Q).rnDeriv ν p.swap) ((π ⊗ₘ Q).rnDeriv ν p)) := 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. 8, proof of Proposition 5 (first two lines of the display)
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