Reference · Finite types, distributions and Markov chains

rainbow.math.finite.index-hastings-coefficient

Finite types, distributions and Markov chainssrc/rainbow/math/finite/index_hastings_coefficient.clj1 definitions, 2 theorems

Explicit proper Dobrushin factors for canonical Hastings on Index(n+1). Proposal normalization and the executable full-support verdict discharge the coefficient bound. Target normalization is not needed for this bound. Proof terms are checked by the focused gate; no sampler correctness claim.

mcmc/nnrat-hastings-index-contraction-factor :
  (predecessor : ℕ) (target : finite/Index (data/succ predecessor) → ℚ≥0)
  (proposal : finite/Index (data/succ predecessor) → finite/Index (data/succ predecessor) → ℚ≥0)
  → ℚ≥0

mcmc/nnrat-hastings-index-contraction-factor-proper :
  (predecessor : ℕ) (target : finite/Index (data/succ predecessor) → ℚ≥0)
  (proposal : finite/Index (data/succ predecessor) → finite/Index (data/succ predecessor) → ℚ≥0)
  → nnrat/numerator (make) ≤ nnrat/denominator-predecessor (make)
  where make := nnrat/make (nnrat/denominator-predecessor (markov/nnrat-kernel-minimum (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) (mcmc/nnrat-hastings-canonical-kernel (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) target proposal (finite/index-decide-equality (data/succ predecessor))) (finite/index-last predecessor) (finite/index-last predecessor))) (nnrat/denominator-predecessor (markov/nnrat-kernel-minimum (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) (mcmc/nnrat-hastings-canonical-kernel (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) target proposal (finite/index-decide-equality (data/succ predecessor))) (finite/index-last predecessor) (finite/index-last predecessor)))

mcmc/nnrat-hastings-index-dobrushin-bound-of-full-support :
  (predecessor : ℕ) (target : finite/Index (data/succ predecessor) → ℚ≥0)
  (proposal : finite/Index (data/succ predecessor) → finite/Index (data/succ predecessor) → ℚ≥0)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) proposal)
  (full-support : mcmc/full-support-decision (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) target proposal = data/true)
  → markov/signed-kernel-dobrushin-coefficient (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) (mcmc/nnrat-hastings-canonical-kernel (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) target proposal (finite/index-decide-equality (data/succ predecessor))) ≤ signed/from-nnrat (nnrat/make (nnrat/denominator-predecessor (minimum)) (nnrat/denominator-predecessor (minimum)))
  where minimum := markov/nnrat-kernel-minimum (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) (mcmc/nnrat-hastings-canonical-kernel (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor)) target proposal (finite/index-decide-equality (data/succ predecessor))) (finite/index-last predecessor) (finite/index-last predecessor)