Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-contraction-uniqueness

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

Stationary-distribution uniqueness, conditional on one named inequality. This is the ergodic assembly with the Dobrushin step left ABSTRACT: the contraction premise here is exactly the conclusion the in-progress Dobrushin module aims at (one kernel application shrinks total variation by a proper-fraction factor), taken as a hypothesis at the two stationary masses. Nothing about the Dobrushin coefficient is defined or proved here; when that inequality lands, instantiating this theorem is one application, and uniqueness stops being conditional. The proof is the planned composition of the joint lemmas: stationarity feeds the total-variation congruence, so the contraction premise rewrites to TV <= rho * TV at the same pair; the proper-fraction rate-null law forces TV ~ 0; and the separation theorem turns a vanishing total variation into pointwise agreement on the carrier. Native and axiom-free on D63.

Depends onmath.finite.markov-total-variation

markov/nnrat-stationary-pointwise-unique-of-proper-contraction.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  (np dp : ℕ)
  (proper : np ≤ dp)
  (left-stationary : markov/nnrat-stationary S states kernel left)
  (right-stationary : markov/nnrat-stationary S states kernel right)
  (contracts : markov/nnrat-total-variation S states (step₁) (step) ≤ nnrat/make np dp · markov/nnrat-total-variation S states left right)
  (state : S) (member : list/membership S (finset-data/enumeration S states) state)
  → left state = right state
  where step := markov/nnrat-kernel-step S states kernel right
  where step₁ := markov/nnrat-kernel-step S states kernel left