Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-coupling-distance

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

Off-diagonal kernel-row distance bound from a coupling's two marginals. A nonnegative joint mass J with marginals p,q proves L1(pK,qK) <= sum_i sum_j J(i,j)*L1(K(i,-),K(j,-)). No stochastic normalization is needed. The marginal hypotheses are algebraic identities, not the desired distance bound.

Depends onmath.finite.markov-residual-couplingmath.rational.nnrat.weighted-map-sum-distance

markov/nnrat-kernel-step-coupling-distance-bound.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (kernel joint : S → S → ℚ≥0)
  (left-marginal : ∀ (i : S), nnrat/map-sum S (fun j => joint i j) (finset-data/enumeration S states) = left i)
  (right-marginal : ∀ (j : S), nnrat/map-sum S (fun i => joint i j) (finset-data/enumeration S states) = right j)
  → markov/nnrat-total-variation S states (step₁) (step) ≤ 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)
  where step := markov/nnrat-kernel-step S states kernel right
  where step₁ := markov/nnrat-kernel-step S states kernel left

markov/nnrat-kernel-step-positive-residual-coupling-bound.{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)
  → markov/nnrat-total-variation S states (step₂) (step) ≤ nnrat/map-sum S (fun i => nnrat/map-sum S (fun j => coupling i j · markov/nnrat-total-variation S states (kernel i) (kernel j)) (finset-data/enumeration S states)) (finset-data/enumeration S states)
  where coupling := markov/nnrat-product-coupling S states (fun i₁ => nnrat/left-residual-mass (left i₁) (right i₁)) (fun i₁ => nnrat/right-residual-mass (left i₁) (right i₁)) (nnrat/make (data/succ ap) adp)
  where step := markov/nnrat-kernel-step S states kernel right
  where step₂ := markov/nnrat-kernel-step S states kernel left

markov/nnrat-positive-residual-coupling-total.{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)
  → nnrat/map-sum S (fun i => nnrat/map-sum S (fun j => coupling i j) (finset-data/enumeration S states)) (finset-data/enumeration S states) = nnrat/make (data/succ ap) adp
  where coupling := markov/nnrat-product-coupling S states (fun i₁ => nnrat/left-residual-mass (left i₁) (right i₁)) (fun i₁ => nnrat/right-residual-mass (left i₁) (right i₁)) (nnrat/make (data/succ ap) adp)