Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-full-support-irreducible

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_full_support_irreducible.clj0 definitions, 3 theorems

Executable full support certifies irreducibility of finite Index kernels. The full-support decision is executable and its soundness theorem supplies positivity of every canonical Hastings-kernel entry. Generic finite Markov reachability then turns those positive entries into one-step witnesses for every ordered state pair. It also supplies a one-step return at every state, the concrete positive-horizon prerequisite for a future period theorem. The result does not assert aperiodicity, convergence, a spectral gap, or a mixing-time bound. Native and axiom-free on D63.

Depends onmath.finite.markov-full-support

mcmc/nnrat-hastings-index-irreducible-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  → markov/nnrat-irreducible (finite/Index upper) (finite/index-finset upper) (finite/index-decide-equality upper) (kernel)
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)

mcmc/nnrat-hastings-index-return-at-one-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  (state : finite/Index upper)
  → markov/nnrat-return-at (finite/Index upper) (finite/index-finset upper) (finite/index-decide-equality upper) (kernel) state 1
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)

mcmc/nnrat-hastings-index-aperiodic-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  → markov/nnrat-aperiodic (finite/Index upper) (finite/index-finset upper) (finite/index-decide-equality upper) (kernel)
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)