Reference · Finite types, distributions and Markov chains

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

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_total_variation_bound.clj1 definitions, 5 theorems

Normalized finite total variation and its stochastic-row unit bound. The existing total-variation alias denotes L1. Here normalized TV is half that sum. Scalar domination by a+b lifts through the finite sum, giving L1(mu,nu) <= mass(mu)+mass(nu). Two unit masses therefore give TV <= 1. These bounds do not assert contraction or convergence.

Depends onmath.finite.markov-total-variation

markov/nnrat-normalized-total-variation.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  → ℚ≥0

nnrat/distance-at-most-sum :
  (a b : ℚ≥0)
  → nnrat/distance a b ≤ a + b

markov/nnrat-total-variation-at-most-mass-sum.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  → markov/nnrat-total-variation S states left right ≤ probability/nnrat-total-mass S states left + probability/nnrat-total-mass S states right

nnrat/half-times-two-equivalent-one :
  → nnrat/half · (1 + 1) = 1

markov/nnrat-normalized-total-variation-at-most-one.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  (left-normalized : probability/nnrat-total-mass S states left = 1)
  (right-normalized : probability/nnrat-total-mass S states right = 1)
  → markov/nnrat-normalized-total-variation S states left right ≤ 1

markov/row-total-variation-at-most-one.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel) (x y : S)
  → markov/nnrat-normalized-total-variation S states (kernel x) (kernel y) ≤ 1