Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-dobrushin-statement

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_dobrushin_statement.clj1 definitions, 0 theorems

Formal proposition for the finite Dobrushin contraction estimate. Registering this definition checks that the proposition is well formed. It does not inhabit that proposition or add a contraction axiom. The inhabitant is supplied separately by finite-markov-dobrushin-contraction.

Depends onmath.finite.markov-dobrushin-kernel

markov/nnrat-dobrushin-contraction-estimate.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
  → Prop