Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-residual-coupling

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

Residual mass balance and constructive product-coupling marginals. The positive-mass coupling is p(i)*q(j)/M. Its marginals follow by finite-sum scaling and positive reciprocal cancellation. Positivity is explicit; the zero-mass case is not silently divided through.

Depends onmath.finite.markov-residual-expansion

markov/nnrat-product-coupling.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (normalizer : ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

markov/nnrat-left-residual-plus-common-total.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  → probability/nnrat-total-mass S states (fun i => nnrat/left-residual-mass (left i) (right i)) + probability/nnrat-total-mass S states (fun i => minmax/min (left i) (right i)) = probability/nnrat-total-mass S states left

markov/nnrat-residual-totals-equal.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0)
  (same-total : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
  → probability/nnrat-total-mass S states (fun i => nnrat/left-residual-mass (left i) (right i)) = probability/nnrat-total-mass S states (fun i => nnrat/right-residual-mass (left i) (right i))

markov/nnrat-total-variation-is-residual-total-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 (fun i => nnrat/left-residual-mass (left i) (right i)) + probability/nnrat-total-mass S states (fun i => nnrat/right-residual-mass (left i) (right i))

markov/nnrat-product-coupling-left-marginal.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (ap adp : ℕ)
  (other-total : probability/nnrat-total-mass S states right = nnrat/make (data/succ ap) adp)
  (index : S)
  → nnrat/map-sum S (fun i => coupling i) (finset-data/enumeration S states) = left index
  where coupling := markov/nnrat-product-coupling S states left right (nnrat/make (data/succ ap) adp) index

markov/nnrat-product-coupling-right-marginal.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (ap adp : ℕ)
  (other-total : probability/nnrat-total-mass S states left = nnrat/make (data/succ ap) adp)
  (index : S)
  → nnrat/map-sum S (fun i => coupling i index) (finset-data/enumeration S states) = right index
  where coupling := markov/nnrat-product-coupling S states left right (nnrat/make (data/succ ap) adp)