Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-dobrushin-kernel

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

Dobrushin coefficient constructed from every pair of enumerated kernel rows. Two finite maxima compute max_{x,y} TV(Kx,Ky), where TV is half-L1. The coefficient dominates every enumerated row pair, is nonnegative, and is at most one for normalized stochastic rows. No mixing estimate is assumed or proved in this module.

Depends onmath.finite.markov-total-variation-bound

markov/signed-kernel-dobrushin-coefficient.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  → ℚ

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

markov/signed-kernel-dobrushin-coefficient-bounded.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (upper : ℚ)
  (zero-upper : 0 ≤ upper)
  (pointwise : ∀ (x : S), ∀ (x-member : membership x), ∀ (y : S), ∀ (y-member : membership y), signed/from-nnrat (markov/nnrat-normalized-total-variation S states (kernel x) (kernel y)) ≤ upper)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ upper
  where membership := list/membership S (finset-data/enumeration S states)

markov/signed-kernel-dobrushin-coefficient-at-most-one.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ 1

markov/row-distance-at-most-dobrushin-coefficient.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (x : S)
  (x-member : membership x) (y : S) (y-member : membership y)
  → signed/from-nnrat (markov/nnrat-normalized-total-variation S states (kernel x) (kernel y)) ≤ markov/signed-kernel-dobrushin-coefficient S states kernel
  where membership := list/membership S (finset-data/enumeration S states)