Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-stationary-iterate

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

A stationary distribution is fixed by every kernel iterate. First brick of the convergence half: pi stationary implies `kernel-iterate n pi ~ pi` pointwise for every n, by induction -- the successor law unfolds one step, the kernel step respects mass equivalence, and stationarity closes the ring. No contraction premise appears anywhere here; this brick is independent of the Dobrushin line and is consumed later when convergence toward the stationary target is stated. Native and axiom-free on D63.

Depends onmath.finite.markov-iteration

markov/nnrat-stationary-iterate-fixed.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (mass-stationary : markov/nnrat-stationary S states kernel mass) (steps : ℕ)
  (target : S)
  → markov/nnrat-kernel-iterate S states kernel steps mass target = mass target