Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-geometric-convergence

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

Iterates converge to the stationary distribution at geometric rate. Brick 3 of the convergence half: under normalized rows and a certified Dobrushin bound rho, the total variation between the n-th iterate of any start distribution and a stationary distribution of equal total mass is at most rho^n times the initial total variation. The proof combines brick 1 (a stationary distribution is fixed by every iterate) with brick 2 (geometric decay between iterate pairs) at the stationary target. Scope, stated so nobody over-quotes it: this is an explicit geometric ENVELOPE toward the stationary target in exact rationals. It is not a mixing-time statement, makes no claim for rho at or above one (the envelope is then vacuous but true), and the rate-null packaging in the analysis vocabulary is deliberately deferred until a consumer needs it. Native and axiom-free on D63.

Depends onmath.finite.markov-geometric-decay

markov/nnrat-kernel-iterate-geometric-convergence-to-stationary.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho)
  (start pi : S → ℚ≥0) (pi-stationary : markov/nnrat-stationary S states kernel pi)
  (equal-total-mass : probability/nnrat-total-mass S states start = probability/nnrat-total-mass S states pi)
  (steps : ℕ)
  → markov/nnrat-total-variation S states (iterate) pi ≤ nnrat/power rho steps · markov/nnrat-total-variation S states start pi
  where iterate := markov/nnrat-kernel-iterate S states kernel steps start