Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-reachability

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_reachability.clj2 definitions, 4 theorems

Finite-step reachability and irreducibility for exact finite Markov kernels. A target is reachable from a source exactly when some natural-number horizon gives positive mass at the target after iterating from the certified point mass at the source. A kernel is irreducible when every ordered state pair is reachable. Reflexivity uses horizon zero; a positive entry uses horizon one; positive trajectories give their indexed horizons; and pointwise-positive kernels are irreducible. These are support results, not mixing-time or convergence-rate claims. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-reachability-witness

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

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

markov/nnrat-reachable-reflexive.{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-reachable S states decision kernel state state

markov/nnrat-reachable-of-positive-entry.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (source target : S) (entry-positive : nnrat/positive (kernel source target))
  → markov/nnrat-reachable S states decision kernel source target

markov/nnrat-reachable-along-positive-trajectory.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (trajectory : ℕ → S)
  (trajectory-member : ∀ (step : ℕ), list/membership S (finset-data/enumeration S states) (trajectory step))
  (edge-positive : ∀ (step : ℕ), nnrat/positive (kernel (trajectory step) (trajectory (data/succ step))))
  (steps : ℕ)
  → markov/nnrat-reachable S states decision kernel (trajectory 0) (trajectory steps)

markov/nnrat-pointwise-positive-implies-irreducible.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (pointwise-positive : ∀ (source : S), ∀ (target : S), nnrat/positive (kernel source target))
  → markov/nnrat-irreducible S states decision kernel