Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-minorization

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_minorization.clj1 definitions, 3 theorems

Finite shared lower-mass certificates for Dobrushin bounds. A minorizing mass may vanish on some columns, so this does not require full positivity of the kernel. Statements concern the listed support.

Depends onmath.finite.markov-overlapmath.rational.nnrat.unit-fraction

markov/nnrat-kernel-minorizes.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (lower-mass : S → ℚ≥0)
  → Prop

markov/nnrat-common-total-at-least-minorizing-mass.{u} :
  (S : Type u) (states : Finset S) (left right lower-mass : S → ℚ≥0)
  (lower-left : ∀ (x : S), ∀ (x-member : membership x), lower-mass x ≤ left x)
  (lower-right : ∀ (x : S), ∀ (x-member : membership x), lower-mass x ≤ right x)
  → probability/nnrat-total-mass S states lower-mass ≤ probability/nnrat-total-mass S states (fun minorization-column => minmax/min (left minorization-column) (right minorization-column))
  where membership := list/membership S (finset-data/enumeration S states)

markov/signed-kernel-dobrushin-at-most-of-minorization.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (lower-mass : S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (minorization : markov/nnrat-kernel-minorizes S states kernel lower-mass) (rho : ℚ≥0)
  (budget : 1 ≤ rho + probability/nnrat-total-mass S states lower-mass)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho

markov/signed-kernel-dobrushin-at-most-of-positive-minorization.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (lower-mass : S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (minorization : markov/nnrat-kernel-minorizes S states kernel lower-mass)
  (positive : nnrat/positive (mass))
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/make (nnrat/denominator-predecessor (mass)) (nnrat/denominator-predecessor (mass)))
  where mass := probability/nnrat-total-mass S states lower-mass