Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-dobrushin-contraction

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_dobrushin_contraction.clj0 definitions, 2 theorems

Inhabitant of the frozen finite Dobrushin contraction predicate. Split the residual total by its rational numerator. The zero case uses mass preservation; the positive case uses the proved product coupling. No contraction premise, positive-mass assumption, or new axiom is added.

Depends onmath.finite.markov-coupling-coefficientmath.finite.markov-dobrushin-statement

markov/nnrat-kernel-step-zero-residual-contraction.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (same-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  (zero-residual-total : probability/nnrat-total-mass S states (fun i => nnrat/left-residual-mass (left i) (right i)) = 0)
  (rho : ℚ≥0)
  → 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

markov/nnrat-dobrushin-contraction.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
  → markov/nnrat-dobrushin-contraction-estimate S states kernel rho