Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-positive-coefficient

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_positive_coefficient.clj0 definitions, 2 theorems

Explicit Dobrushin factors from a positive finite kernel minimum. Kernel-checked and axiom-free on D63. For minimum m=n/(d+1), use epsilon=1/(d+1) on one listed column and rho=d/(d+1). The bound need not be sharp. This module does not assert executable correctness.

Depends onmath.finite.markov-overlapmath.rational.nnrat.unit-fractionmath.finite.markov-kernel-minimum

markov/signed-kernel-dobrushin-at-most-of-positive-minimum.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (initial-source initial-target : S)
  (initial-target-member : list/membership S (finset-data/enumeration S states) initial-target)
  (minimum-positive : nnrat/positive (minimum))
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/make (nnrat/denominator-predecessor (minimum)) (nnrat/denominator-predecessor (minimum)))
  where minimum := markov/nnrat-kernel-minimum S states kernel initial-source initial-target

markov/signed-kernel-dobrushin-at-most-of-listed-positive.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (initial-source initial-target : S)
  (initial-source-member : membership initial-source)
  (initial-target-member : membership initial-target)
  (listed-positive : ∀ (source : S), ∀ (target : S), ∀ (source-member : membership source), ∀ (target-member : membership target), nnrat/positive (kernel source target))
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/make (nnrat/denominator-predecessor (minimum)) (nnrat/denominator-predecessor (minimum)))
  where membership := list/membership S (finset-data/enumeration S states)
  where minimum := markov/nnrat-kernel-minimum S states kernel initial-source initial-target