Reference · Finite types, distributions and Markov chains

rainbow.math.finite.index-hastings-ergodic

Finite types, distributions and Markov chainssrc/rainbow/math/finite/index_hastings_ergodic.clj0 definitions, 2 theorems

The finite ergodic theorem, instantiated for canonical Hastings kernels. For the canonical Metropolis-Hastings kernel on Index(n+1) built from a target and a normalized proposal, the executable full-support verdict alone certifies the Dobrushin factor d/(d+1) (d the kernel minimum's denominator predecessor), and both halves of the abstract theorem pair instantiate: any two equal-total-mass stationary distributions agree pointwise on the carrier, and iterates of any equal-mass start approach a stationary distribution inside the explicit (d/(d+1))^n envelope. Scope, carried from the design notes: the factor is a CERTIFIED rate, not THE rate -- conservative and dependent on the kernel's raw representation -- and nothing here is a mixing-time, spectral-gap, or sampling statement. The factor stays constructor- visible (make d d) throughout; naming it behind an alias makes the conversion checker normalize the symbolic kernel. Native and axiom-free on D63.

Depends onmath.finite.index-hastings-coefficient

mcmc/nnrat-hastings-index-stationary-unique-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)
  (left right : finite/Index (data/succ predecessor) → ℚ≥0)
  (left-stationary : stationary left) (right-stationary : stationary right)
  (equal-total-mass : mass left = mass right)
  (state : finite/Index (data/succ predecessor))
  (member : list/membership (finite/Index (data/succ predecessor)) (enumeration) state)
  → left state = right state
  where enumeration := finset-data/enumeration (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor))
  where mass := probability/nnrat-total-mass (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor))
  where stationary := markov/nnrat-stationary (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)))

mcmc/nnrat-hastings-index-geometric-convergence-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)
  (start pi : finite/Index (data/succ predecessor) → ℚ≥0)
  (pi-stationary : markov/nnrat-stationary (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))) pi)
  (equal-total-mass : mass start = mass pi)
  (steps : ℕ)
  → variation (iterate) pi ≤ nnrat/power (make) steps · variation start pi
  where iterate := markov/nnrat-kernel-iterate (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))) steps start
  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)))
  where mass := probability/nnrat-total-mass (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor))
  where variation := markov/nnrat-total-variation (finite/Index (data/succ predecessor)) (finite/index-finset (data/succ predecessor))