Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-iteration-semigroup

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_iteration_semigroup.clj0 definitions, 1 theorems

Semigroup law for finite exact-rational Markov iteration. Iterating a kernel for m+n steps is equivalent to first iterating for n steps and then for m more. The proof is natural-number induction on m; the successor case lifts the induction hypothesis through one kernel step using pointwise mass congruence. This is the temporal-composition prerequisite for transitive finite-step reachability. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-iteration

markov/nnrat-kernel-iterate-add.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (left right : ℕ) (state : S)
  → markov/nnrat-kernel-iterate S states kernel (algebra/nat-add left right) mass state = markov/nnrat-kernel-iterate S states kernel left (fun middle => iterate middle) state
  where iterate := markov/nnrat-kernel-iterate S states kernel right mass