Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-metropolis-hastings

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_metropolis_hastings.clj5 definitions, 8 theorems

A fully checked finite Metropolis--Hastings independence sampler. The worked target on states {0,1} is (1/3,2/3). Its independence proposal equals the target, so the Hastings ratio is one and every proposal is accepted. The resulting kernel is the target row at every source. We prove exact row normalization, detailed balance, stationarity, and one-step mixing from every normalized initial mass. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-cesaro

mcmc/mh-two-state-space :
  → Finset ℕ

mcmc/mh-target-mass :
  (x₁ : ℕ)
  → ℚ≥0

mcmc/mh-independence-proposal :
  (x₁ x₂ : ℕ)
  → ℚ≥0

mcmc/mh-acceptance :
  (x₁ x₂ : ℕ)
  → ℚ≥0

mcmc/mh-kernel :
  (x₁ x₂ : ℕ)
  → ℚ≥0

mcmc/mh-target-normalized :
  → probability/nnrat-total-mass ℕ ahof-d2/grid mcmc/mh-target-mass = 1

mcmc/mh-proposal-normalized :
  (source : ℕ)
  → probability/nnrat-total-mass ℕ ahof-d2/grid (mcmc/mh-independence-proposal source) = 1

mcmc/mh-all-proposals-accepted :
  (source target : ℕ)
  → mcmc/mh-acceptance source target = 1

mcmc/mh-kernel-equals-proposal :
  (source target : ℕ)
  → mcmc/mh-kernel source target = mcmc/mh-independence-proposal source target

mcmc/mh-kernel-rows-normalized :
  → markov/nnrat-kernel-rows-normalized ℕ ahof-d2/grid mcmc/mh-kernel

mcmc/mh-detailed-balance :
  → markov/nnrat-detailed-balance ℕ mcmc/mh-target-mass mcmc/mh-kernel

mcmc/mh-target-stationary :
  → markov/nnrat-stationary ℕ ahof-d2/grid mcmc/mh-kernel mcmc/mh-target-mass

mcmc/mh-mixes-in-one-step :
  (initial : ℕ → ℚ≥0)
  (initial-normalized : probability/nnrat-total-mass ℕ ahof-d2/grid initial = 1)
  (target : ℕ)
  → markov/nnrat-kernel-step ℕ ahof-d2/grid mcmc/mh-kernel initial target = mcmc/mh-target-mass target