Measure-level domination:
ProvedTierneyMH.Mixture.mixture_measure_dominationLet be a probability measure on , let be a finite or countable family of Markov proposal kernels, and let with . Let be the mixture proposal, let be the maximal acceptance probability for and the one for (all for the target ). Then, as measures on ,
that is, the inequality holds when both sides are evaluated on any measurable set .
This is the whole computation of the proof of Proposition 5. It compares the accepted parts of one step of the two samplers: the Metropolis–Hastings sampler with the mixture proposal accepts at least as much mass, set by set in the joint law of current and next state, as the mixture of the component samplers.
Formalization Note Weights are in ℝ≥0 with HasSum β 1; the index type is countable. No hypothesis on the σ-algebra of is needed at this measure level.
import Mathlib import Definitions.Def_TierneyMH_Mixture_alphaMH import Definitions.Def_TierneyMH_Mixture_mixKernel open MeasureTheory ProbabilityTheory open scoped ENNReal NNReal
namespace TierneyMH.Mixture
/-- **Measure-level domination** (Tierney 1998, proof of Proposition 5, p. 8, the whole
display). Let `Qᵢ` be a countable family of Markov proposal kernels and `βᵢ ≥ 0` weights with
`∑ βᵢ = 1`, `Q = ∑ βᵢ Qᵢ`, and let `α_MH`, `α_MH^{(i)}` be the maximal acceptance probabilities
for `Q`, `Qᵢ` and the target `π`. Then, as measures on `E × E`,
`π(dx) Q(x, dy) α_MH(x, y) ≥ ∑ βᵢ π(dx) Qᵢ(x, dy) α_MH^{(i)}(x, y)`,
i.e. the inequality holds on every measurable `S ⊆ E × E`. -/
theorem mixture_measure_domination {E : Type*} [MeasurableSpace E]
(π : Measure E) [IsProbabilityMeasure π]
{ι : Type*} [Countable ι] (Q : ι → Kernel E E) [∀ i, IsMarkovKernel (Q i)]
(β : ι → ℝ≥0) (hβ : HasSum β 1) (S : Set (E × E)) (hS : MeasurableSet S) :
∑' i, (β i : ℝ≥0∞) * ((π ⊗ₘ Q i).withDensity (alphaMH π (Q i))) S ≤
((π ⊗ₘ mixKernel β Q).withDensity (alphaMH π (mixKernel β Q))) S := by sorry
end TierneyMH.Mixture
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.