Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-column-exact-contraction

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_column_exact_contraction.clj0 definitions, 7 theorems

Exact column-minimum coefficient and its positive-total properness.

Depends onmath.finite.markov-ergodic-uniquenessmath.finite.markov-geometric-convergencemath.finite.markov-geometric-decaymath.finite.markov-dobrushin-contractionmath.finite.markov-column-minorizationmath.finite.markov-minorization-complementmath.rational.nnrat.complement-proper

markov/nnrat-exact-minorization-factor-proper.{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)
  (positive : nnrat/positive (probability/nnrat-total-mass S states lower-mass))
  → nnrat/numerator (distance) ≤ nnrat/denominator-predecessor (distance)
  where distance := nnrat/distance (probability/nnrat-total-mass S states lower-mass) 1

markov/signed-kernel-dobrushin-at-most-of-exact-column-minimum.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat (nnrat/distance (mass) 1)
  where mass := probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)

markov/nnrat-exact-column-minimum-factor-proper.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (positive : nnrat/positive (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)))
  → nnrat/numerator (distance) ≤ nnrat/denominator-predecessor (distance)
  where distance := nnrat/distance (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)) 1

markov/nnrat-exact-column-minimum-contraction.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (left right : S → ℚ≥0)
  (equal-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  → markov/nnrat-total-variation S states (step₂) (step) ≤ nnrat/distance (mass) 1 · markov/nnrat-total-variation S states left right
  where mass := probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)
  where step := markov/nnrat-kernel-step S states kernel right
  where step₂ := markov/nnrat-kernel-step S states kernel left

markov/nnrat-exact-column-minimum-geometric-decay.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (left right : S → ℚ≥0)
  (equal-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  (steps : ℕ)
  → markov/nnrat-total-variation S states (iterate₂) (iterate) ≤ nnrat/power (distance) steps · markov/nnrat-total-variation S states left right
  where distance := nnrat/distance (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)) 1
  where iterate := markov/nnrat-kernel-iterate S states kernel steps right
  where iterate₂ := markov/nnrat-kernel-iterate S states kernel steps left

markov/nnrat-exact-column-minimum-stationary-pointwise-unique.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : membership anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (positive : nnrat/positive (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)))
  (proper : nnrat/numerator (distance) ≤ nnrat/denominator-predecessor (distance))
  (left right : S → ℚ≥0)
  (left-stationary : markov/nnrat-stationary S states kernel left)
  (right-stationary : markov/nnrat-stationary S states kernel right)
  (equal-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  (state : S) (state-member : membership state)
  → left state = right state
  where distance := nnrat/distance (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)) 1
  where membership := list/membership S (finset-data/enumeration S states)

markov/nnrat-exact-column-minimum-geometric-convergence-to-stationary.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (anchor : S)
  (anchor-member : list/membership S (finset-data/enumeration S states) anchor)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (start pi : S → ℚ≥0) (pi-stationary : markov/nnrat-stationary S states kernel pi)
  (equal-total : probability/nnrat-total-mass S states start = probability/nnrat-total-mass S states pi)
  (steps : ℕ)
  → markov/nnrat-total-variation S states (iterate) pi ≤ nnrat/power (distance) steps · markov/nnrat-total-variation S states start pi
  where distance := nnrat/distance (probability/nnrat-total-mass S states (markov/nnrat-column-minimum-mass S states kernel anchor)) 1
  where iterate := markov/nnrat-kernel-iterate S states kernel steps start