Prove2Me

Proposition 1: symmetric decomposition of a σ\sigma-finite measure on E×EE\times E against its transpose

Proved
TierneyMH.Reversibility.proposition1_symmetric_split

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

measure-theorymetropolis-hastingsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1radon-nikodym

Let μ\mu be a σ\sigma-finite measure on the product space (E×E,E⊗E)(E\times E,\mathcal E\otimes\mathcal E) and let μT(dx,dy)=μ(dy,dx)\mu^T(dx,dy)=\mu(dy,dx). Then:

  1. Existence. There is a symmetric set R∈E⊗ER\in\mathcal E\otimes\mathcal E such that μ\mu and μT\mu^T are mutually absolutely continuous on RR and mutually singular on RcR^c.
  2. Uniqueness. If RR and R′R' both have these properties, then their symmetric difference is null for both measures:
μ(R △ R′)=0andμT(R △ R′)=0.\mu(R\,\triangle\,R')=0\quad\text{and}\quad \mu^T(R\,\triangle\,R')=0.
  1. Density. For every such RR there is a version rr of the density r(x,y)=μR(dx,dy)/μRT(dx,dy)r(x,y)=\mu_R(dx,dy)/\mu^T_R(dx,dy) 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 decomposition, applied to μ(dx,dy)=π(dx)Q(x,dy)\mu(dx,dy)=\pi(dx)Q(x,dy), supplies the set RR and the function rr in which Theorem 2's conditions are stated; its existence part guarantees that Theorem 2 is not vacuous.

Formalization Note The set conditions are the definition IsSymmetricSplit and the density conditions IsRatioVersion; μT\mu^T is μ.map Prod.swap.

Preamble
import Mathlib
import Definitions.Def_TierneyMH_Shared_IsSymmetricSplit
import Definitions.Def_TierneyMH_Shared_IsRatioVersion

open TierneyMH.Shared

open MeasureTheory
open scoped ENNReal
Formal statement
namespace TierneyMH.Reversibility

/-- **Proposition 1** (Tierney 1998, p. 2). Let `μ` be a σ-finite measure on `E × E` (with the
product σ-algebra) and `μᵀ = μ.map Prod.swap`. Then
1. there is a symmetric measurable set `R` on which `μ` and `μᵀ` are mutually absolutely
   continuous and on whose complement they are mutually singular;
2. such an `R` is unique up to sets null for both `μ` and `μᵀ`;
3. for such an `R`, the density `r = dμ_R / dμᵀ_R` has a version with `0 < r < ∞` and
   `r(x, y) = 1 / r(y, x)` for all `x, y`. -/
theorem proposition1_symmetric_split {E : Type*} [MeasurableSpace E]
    (μ : Measure (E × E)) [SigmaFinite μ] :
    (∃ R, IsSymmetricSplit μ R) ∧
    (∀ R R', IsSymmetricSplit μ R → IsSymmetricSplit μ R' →
      μ (symmDiff R R') = 0 ∧ (μ.map Prod.swap) (symmDiff R R') = 0) ∧
    (∀ R, IsSymmetricSplit μ R → ∃ r : E × E → ℝ≥0∞, IsRatioVersion μ R r) := by sorry

end TierneyMH.Reversibility
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
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