Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-total-variation-translation

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

Common finite mass cancels from L1 and normalized total variation. This removes a shared component before bounding the remaining mass in the Dobrushin proof. No normalization or disjointness premise is needed here.

Depends onmath.finite.markov-total-variation-boundmath.rational.nnrat.distance-translation

markov/nnrat-total-variation-common-mass.{u} :
  (S : Type u) (states : Finset S) (left right common : S → ℚ≥0)
  → markov/nnrat-total-variation S states (fun state => left state + common state) (fun state => right state + common state) = markov/nnrat-total-variation S states left right

markov/nnrat-normalized-total-variation-common-mass.{u} :
  (S : Type u) (states : Finset S) (left right common : S → ℚ≥0)
  → variation (fun state => left state + common state) (fun state => right state + common state) = variation left right
  where variation := markov/nnrat-normalized-total-variation S states