Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-column-minorization

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

Construct a shared lower mass by taking a finite minimum in each column. With a listed anchor it is the greatest listed minorizing mass pointwise. A positive computed total supplies a certified proper Dobrushin factor.

Depends onmath.finite.markov-minorizationmath.finite.rational-argmin

markov/nnrat-column-minimum-mass.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor x₁ : S)
  → ℚ≥0

markov/nnrat-column-minimum-mass-minorizes.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  → markov/nnrat-kernel-minorizes S states kernel (mass)
  where mass := markov/nnrat-column-minimum-mass S states kernel anchor

markov/nnrat-column-minimum-mass-greatest.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : membership anchor) (lower-mass : S → ℚ≥0)
  (minorization : markov/nnrat-kernel-minorizes S states kernel lower-mass) (column : S)
  (column-member : membership column)
  → lower-mass column ≤ markov/nnrat-column-minimum-mass S states kernel anchor column
  where membership := list/membership S (finset-data/enumeration S states)

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

markov/signed-kernel-dobrushin-at-most-of-positive-column-minimum.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (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 (markov/nnrat-column-minimum-mass S states kernel anchor)