Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-total-variation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_total_variation.clj1 definitions, 6 theorems

Total-variation distance between finite exact-rational distributions, and the separation half of the coming ergodic theorem. The ergodic-hypotheses bundle is packaged and discharged by computation; the theorem those hypotheses exist for still is not stated. Its classical proof runs through a metric on distributions, and this module is the bridgehead: the L1 distance over the enumeration -- the sum of pointwise exact distances -- with the lemmas that make ZERO distance mean something. What is proved: the distance is a congruence for pointwise equivalence (the rewrite that turns TV(mu K, nu K) into TV(mu, nu) under stationarity); it is symmetric; it vanishes on pointwise- equivalent distributions; and -- the load-bearing direction -- a vanishing distance forces pointwise equivalence AT EVERY ENUMERATED STATE, through a new generic lemma that a zero finite sum has zero listed terms. The capstone packages the separation half of uniqueness: two stationary distributions at total-variation zero agree pointwise on the carrier. What is deliberately NOT here, so nobody reads the bridgehead as the bridge: no contraction inequality. The classical Dobrushin step -- one kernel application shrinks this distance by a factor below one under the certified positive minimum -- is the single remaining inequality between these lemmas and stationary-distribution uniqueness, and it is unproved. The reduction is the point: uniqueness now rests on exactly one named open inequality rather than on a theory that did not exist. Native and axiom-free on D63.

Depends onmath.finite.markov-stationarity

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

nnrat/map-sum-zero-of-member.{u} :
  (A : Type u) (f : A → ℚ≥0) (items : List A)
  (h₁ : nnrat/map-sum A f items = 0)
  (value : A) (member : list/membership A items value)
  → f value = 0

markov/nnrat-total-variation-respects-pointwise-equivalent.{u} :
  (S : Type u) (states : Finset S)
  (left equivalent-left right equivalent-right : S → ℚ≥0)
  (agree-left : ∀ (state : S), left state = equivalent-left state)
  (agree-right : ∀ (state : S), right state = equivalent-right state)
  → markov/nnrat-total-variation S states left right = markov/nnrat-total-variation S states equivalent-left equivalent-right

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

markov/nnrat-total-variation-zero-of-pointwise-equivalent.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  (agree : ∀ (state : S), left state = right state)
  → markov/nnrat-total-variation S states left right = 0

markov/nnrat-total-variation-zero-implies-pointwise-equivalent.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  (vanishes : markov/nnrat-total-variation S states left right = 0)
  (state : S) (member : list/membership S (finset-data/enumeration S states) state)
  → left state = right state

markov/nnrat-stationary-pointwise-unique-of-total-variation-zero.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  (left-stationary : markov/nnrat-stationary S states kernel left)
  (right-stationary : markov/nnrat-stationary S states kernel right)
  (vanishes : markov/nnrat-total-variation S states left right = 0)
  (state : S) (member : list/membership S (finset-data/enumeration S states) state)
  → left state = right state