Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-dobrushin

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_dobrushin.clj1 definitions, 4 theorems

Maximum of a supplied NNRAT distance list, for a finite Dobrushin coefficient. The list fold and its conditional bounds are checked here. Complete row coefficients and contraction are proved in finite-markov-dobrushin-kernel and finite-markov-dobrushin-contraction; metadata below points to them.

Depends onmath.rational.signed.rationalmath.rational.signed.ordermath.rational.signed.vector-sup-distancemath.rational.signed.unit-laws

markov/signed-dobrushin-coefficient.{u} :
  (S : Type u) (distances : List ℚ≥0)
  → ℚ

markov/signed-dobrushin-coefficient-nonnegative.{u} :
  (S : Type u) (distances : List ℚ≥0)
  → 0 ≤ markov/signed-dobrushin-coefficient S distances

markov/signed-dobrushin-coefficient-empty.{u} :
  (S : Type u)
  → markov/signed-dobrushin-coefficient S [] = 0

markov/signed-dobrushin-coefficient-bounded.{u} :
  (S : Type u) (distances : List ℚ≥0) (upper : ℚ)
  (zero-upper : 0 ≤ upper)
  (pointwise : ∀ (distance : ℚ≥0), ∀ (member : list/membership ℚ≥0 distances distance), signed/from-nnrat distance ≤ upper)
  → markov/signed-dobrushin-coefficient S distances ≤ upper

markov/signed-dobrushin-coefficient-at-most-one-of-pointwise.{u} :
  (S : Type u) (distances : List ℚ≥0)
  (pointwise : ∀ (distance : ℚ≥0), ∀ (member : list/membership ℚ≥0 distances distance), signed/from-nnrat distance ≤ 1)
  → markov/signed-dobrushin-coefficient S distances ≤ 1