Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-ergodic-uniqueness

Finite types, distributions and Markov chains src/rainbow/math/finite/markov_ergodic_uniqueness.clj0 definitions, 1 theorems

Uniqueness of stationary distributions under a certified Dobrushin bound. The unconditional capstone: for a finite kernel whose Dobrushin coefficient is at most a structural proper fraction np/(dp+1), any two stationary mass functions of equal total mass agree pointwise on the carrier. The proof is one application of the contraction inhabitant to discharge the conditional uniqueness theorem's premise at the two stationary masses -- the composition specified in the design notes, now with no open inequality anywhere beneath it. Native and axiom-free on D63.

Depends onmath.finite.markov-dobrushin-contraction

markov/nnrat-stationary-pointwise-unique-of-dobrushin-bound

TheoremFor all inputsNo axiomsSource, line 58

markov/nnrat-stationary-pointwise-unique-of-dobrushin-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (np dp : ℕ)
  (proper : np ≤ dp)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/make np dp))
  (left right : S → ℚ≥0)
  (left-stationary : markov/nnrat-stationary S states kernel left)
  (right-stationary : markov/nnrat-stationary S states kernel right)
  (equal-total-mass : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  (state : S) (member : list/membership S (finset-data/enumeration S states) state)
  → left state = right state

= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational≤ = signed/at-most