Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-overlap

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_overlap.clj0 definitions, 6 theorems

Shared-mass certificates for finite Dobrushin bounds. Equal input total mass gives normalized TV + common mass = input mass. For probability rows, a lower bound on common mass certifies an upper bound on the all-pairs coefficient, without rational subtraction.

Depends onmath.finite.markov-residual-couplingmath.finite.markov-dobrushin-kernelmath.rational.nnrat.map-sum-member

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

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

markov/nnrat-normalized-tv-at-most-of-common-mass.{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)
  (rho : ℚ≥0)
  (overlap-budget : 1 ≤ rho + probability/nnrat-total-mass S states (fun overlap-state => minmax/min (left overlap-state) (right overlap-state)))
  → markov/nnrat-normalized-total-variation S states left right ≤ rho

markov/nnrat-common-total-at-least-listed-term.{u} :
  (S : Type u) (states : Finset S) (left right : S → ℚ≥0) (target : S)
  (target-member : list/membership S (finset-data/enumeration S states) target)
  (epsilon : ℚ≥0)
  (left-bound : epsilon ≤ left target)
  (right-bound : epsilon ≤ right target)
  → epsilon ≤ probability/nnrat-total-mass S states (fun overlap-state => minmax/min (left overlap-state) (right overlap-state))

markov/signed-kernel-dobrushin-at-most-of-common-mass.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel) (rho : ℚ≥0)
  (overlap-budget : ∀ (i : S), ∀ (i-member : membership i), ∀ (j : S), ∀ (j-member : membership j), 1 ≤ rho + probability/nnrat-total-mass S states (fun overlap-state => minmax/min (kernel i overlap-state) (kernel j overlap-state)))
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho
  where membership := list/membership S (finset-data/enumeration S states)

markov/signed-kernel-dobrushin-at-most-of-shared-column.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel) (target : S)
  (target-member : membership target) (epsilon rho : ℚ≥0)
  (column-bound : ∀ (i : S), ∀ (i-member : membership i), epsilon ≤ kernel i target)
  (budget : 1 ≤ rho + epsilon)
  → markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho
  where membership := list/membership S (finset-data/enumeration S states)