Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-return-time

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

Fixed-horizon return evidence for exact finite Markov kernels. `markov/nnrat-return-at` says that iteration from the canonical point mass at a state has positive mass back at that same state after the stated natural horizon. Every state returns at horizon zero, and a positive self-loop gives a return at horizon one. A future period definition must explicitly restrict to positive horizons; these facts alone do not claim aperiodicity or mixing. Native and axiom-free on D63.

Depends onmath.finite.markov-point-mass

markov/nnrat-return-at.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (x₁ : S) (x₂ : ℕ)
  → Prop

markov/nnrat-return-at-zero.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (state : S)
  → markov/nnrat-return-at S states decision kernel state 0

markov/nnrat-return-at-one-of-positive-self-loop.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision) (state : S)
  (self-loop-positive : nnrat/positive (kernel state state))
  → markov/nnrat-return-at S states decision kernel state 1