Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-mixture-statement

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

Formal target for the finite residual-mixture inequality used by Dobrushin. This is deliberately a proposition declaration: the finite sum inequality is not claimed until its constructive proof is registered.

Depends onmath.finite.markov-dobrushin-kernel

markov/nnrat-finite-mixture-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (rho weighted-sum weight-total : ℚ≥0)
  → Prop