Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-ergodic-hypotheses

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_ergodic_hypotheses.clj1 definitions, 3 theorems

The exact finite-chain hypotheses needed by a future ergodic theorem. `markov/nnrat-ergodic-hypotheses` packages row normalization, irreducibility, and aperiodicity. It is deliberately named hypotheses: this module does not claim convergence, uniqueness, a rate, or a mixing bound. For canonical Hastings kernels on Index n, proposal normalization proves row normalization, while the executable full-support verdict proves the other two fields. Native and axiom-free on D63.

Depends onmath.finite.markov-full-support-irreducible

markov/nnrat-ergodic-hypotheses.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  → Prop

mcmc/nnrat-hastings-index-canonical-kernel-rows-normalized :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (proposal-normalized : normalized proposal)
  → normalized (kernel)
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)
  where normalized := markov/nnrat-kernel-rows-normalized (finite/Index upper) (finite/index-finset upper)

mcmc/nnrat-hastings-index-ergodic-hypotheses-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized (finite/Index upper) (finite/index-finset upper) proposal)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  → markov/nnrat-ergodic-hypotheses (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-stationary-and-ergodic-hypotheses-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (target-normalized : probability/nnrat-total-mass (finite/Index upper) (finite/index-finset upper) target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized (finite/Index upper) (finite/index-finset upper) proposal)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  → proposition/conjunction (stationary) (hypotheses)
  where hypotheses := markov/nnrat-ergodic-hypotheses (finite/Index upper) (finite/index-finset upper) (finite/index-decide-equality upper) (mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper))
  where stationary := markov/nnrat-stationary (finite/Index upper) (finite/index-finset upper) (mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)) target