Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-minorization-complement

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_minorization_complement.clj0 definitions, 3 theorems

Exact complementary-mass bounds, without a raw-denominator approximation. A listed normalized row bounds the shared total before taking its complement.

Depends onmath.finite.markov-minorizationmath.rational.nnrat.ordered-distance

markov/nnrat-minorizing-total-at-most-one.{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) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  → probability/nnrat-total-mass S states lower-mass ≤ 1

nnrat/one-at-most-distance-complement-plus-mass :
  (mass : ℚ≥0)
  (bounded : mass ≤ 1)
  → 1 ≤ nnrat/distance mass 1 + mass

markov/signed-kernel-dobrushin-at-most-of-exact-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) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/distance (mass) 1)
  where mass := probability/nnrat-total-mass S states lower-mass