Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-coupling-coefficient

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

Charge off-diagonal residual coupling costs to the Dobrushin coefficient. Positive residual mass is explicit here; the zero branch is separate.

Depends onmath.finite.markov-coupling-distancemath.finite.markov-dobrushin-kernelmath.rational.nnrat.map-sum-on

markov/nnrat-row-l1-at-most-twice-dobrushin-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
  (coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho)
  (i : S) (i-member : membership i) (j : S) (j-member : membership j)
  → markov/nnrat-total-variation S states (kernel i) (kernel j) ≤ (1 + 1) · rho
  where membership := list/membership S (finset-data/enumeration S states)

markov/nnrat-coupling-row-cost-at-most-dobrushin-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
  (coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho)
  (joint : S → S → ℚ≥0)
  → nnrat/map-sum S (fun i => nnrat/map-sum S (fun j => joint i j · markov/nnrat-total-variation S states (kernel i) (kernel j)) (finset-data/enumeration S states)) (finset-data/enumeration S states) ≤ nnrat/map-sum S (fun i => nnrat/map-sum S (fun j => joint i j) (finset-data/enumeration S states)) (finset-data/enumeration S states) · ((1 + 1) · rho)

markov/nnrat-kernel-step-positive-residual-contraction.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (kernel : S → S → ℚ≥0)
  (ap adp : ℕ)
  (same-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  (positive-residual-total : probability/nnrat-total-mass S states (fun i => nnrat/left-residual-mass (left i) (right i)) = nnrat/make (data/succ ap) adp)
  (rho : ℚ≥0)
  (coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho)
  → markov/nnrat-total-variation S states (step₁) (step) ≤ rho · markov/nnrat-total-variation S states left right
  where step := markov/nnrat-kernel-step S states kernel right
  where step₁ := markov/nnrat-kernel-step S states kernel left