Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-aperiodicity

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_aperiodicity.clj2 definitions, 2 theorems

Aperiodicity from exact finite-state return horizons. A state is aperiodic when every natural divisor common to all of its positive return horizons also divides one. This is the gcd-one definition expressed without adding a gcd operator to the trusted language. A kernel is aperiodic when every state is. A return at horizon one discharges the common-divisor condition directly. No convergence rate or mixing theorem is claimed. Native and axiom-free on D63.

Depends onmath.finite.markov-return-timemath.nat.divisibility

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

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

markov/nnrat-aperiodic-at-of-return-at-one.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (state : S) (returns-at-one : markov/nnrat-return-at S states decision kernel state 1)
  → markov/nnrat-aperiodic-at S states decision kernel state

markov/nnrat-aperiodic-of-all-return-at-one.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (all-return-at-one : ∀ (state : S), markov/nnrat-return-at S states decision kernel state 1)
  → markov/nnrat-aperiodic S states decision kernel