Prove2Me

Proposition 1 via its proof: R={h(x,y)>0,h(y,x)>0}R=\{h(x,y)>0,h(y,x)>0\} and r=h(x,y)/h(y,x)r=h(x,y)/h(y,x) satisfy Proposition 1 for π(dx)Q(x,dy)\pi(dx)Q(x,dy)

Proved
TierneyMH.Mixture.proposition1_canonical_split

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 on (E,E)(E,\mathcal E), let QQ be a Markov kernel on EE, and let μ(dx,dy)=π(dx)Q(x,dy)\mu(dx,dy)=\pi(dx)Q(x,dy), μT(dx,dy)=μ(dy,dx)\mu^T(dx,dy)=\mu(dy,dx). Let h=dμ/d(μ+μT)h=d\mu/d(\mu+\mu^T),

R={(x,y):h(x,y)>0 and h(y,x)>0},r(x,y)={h(x,y)/h(y,x),(x,y)∈R,1,(x,y)∉R.R=\{(x,y): h(x,y)>0\text{ and } h(y,x)>0\},\qquad r(x,y)=\begin{cases}h(x,y)/h(y,x), & (x,y)\in R,\\ 1,&(x,y)\notin R.\end{cases}

Then:

  1. R∈E⊗ER\in\mathcal E\otimes\mathcal E is symmetric, μ\mu and μT\mu^T are mutually absolutely continuous on RR and mutually singular on RcR^c;
  2. rr is a measurable version of the density dμR/dμRTd\mu_R/d\mu^T_R with 0<r(x,y)<∞0<r(x,y)<\infty and r(x,y)=1/r(y,x)r(x,y)=1/r(y,x) for all x,y∈Ex,y\in E.

This is the construction in the proof of Proposition 1, specialized to the measure μ=π⊗Q\mu=\pi\otimes Q of a Metropolis–Hastings algorithm. It certifies that the set and ratio from which αMH\alpha_{MH} is built are the paper's RR and rr.

Formalization Note The ratio is set to 11 also on the (μ+μT)(\mu+\mu^T)-null subset of RR where hh is infinite, so that condition 2 holds at every point (see canonRatio). The paper states Proposition 1 for every σ\sigma-finite μ\mu; here μ\mu is the finite measure π⊗Q\pi\otimes Q, the only case the mission uses.

Preamble
import Mathlib
import Definitions.Def_TierneyMH_Shared_IsSymmetricSplit
import Definitions.Def_TierneyMH_Shared_IsRatioVersion
import Definitions.Def_TierneyMH_Mixture_canonR
import Definitions.Def_TierneyMH_Mixture_canonRatio

open TierneyMH.Shared

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

/-- **Proposition 1, via its proof** (Tierney 1998, p. 2), for `μ(dx, dy) = π(dx) Q(x, dy)`.
With `ν = μ + μᵀ`, `h = dμ/dν`, `R = {(x, y) : h(x, y) > 0 and h(y, x) > 0}` (`canonR π Q`)
and `r = h(x, y)/h(y, x)` on `R`, `r = 1` on `Rᶜ` (`canonRatio π Q`):
`R` is a symmetric measurable set on which `μ` and `μᵀ` are mutually absolutely continuous and
off which they are mutually singular, and `r` is a version of `dμ_R/dμᵀ_R` with
`0 < r < ∞` and `r(x, y) = 1/r(y, x)` everywhere. -/
theorem proposition1_canonical_split {E : Type*} [MeasurableSpace E]
    (π : Measure E) [IsProbabilityMeasure π] (Q : Kernel E E) [IsMarkovKernel Q] :
    IsSymmetricSplit (π ⊗ₘ Q) (canonR π Q) ∧
      IsRatioVersion (π ⊗ₘ Q) (canonR π Q) (canonRatio π 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. 2, Proposition 1 and its proof
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