Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-residual-expansion

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_residual_expansion.clj0 definitions, 5 theorems

Canonical common mass cancels after a kernel step. For c=min(left,right), p=left residual and q=right residual: step(left) ~ step(p)+step(c), step(right) ~ step(q)+step(c); L1(step(left),step(right)) ~ L1(step(p),step(q)). Opening the residual sums gives a double-sum distance upper bound. These laws hold for every finite nonnegative kernel; normalization and equal total mass are not needed. The all-pairs Dobrushin estimate is a later step.

Depends onmath.finite.markov-total-variation-translationmath.rational.nnrat.shared-residual-massmath.rational.nnrat.ring

markov/nnrat-kernel-step-left-residual-decomposition.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  (target : S)
  → step left target = step (fun i => nnrat/left-residual-mass (left i) (right i)) target + step (fun i => minmax/min (left i) (right i)) target
  where step := markov/nnrat-kernel-step S states kernel

markov/nnrat-kernel-step-right-residual-decomposition.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  (target : S)
  → step right target = step (fun i => nnrat/right-residual-mass (left i) (right i)) target + step (fun i => minmax/min (left i) (right i)) target
  where step := markov/nnrat-kernel-step S states kernel

markov/nnrat-kernel-step-total-variation-residual.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  → markov/nnrat-total-variation S states (step₃) (step₂) = markov/nnrat-total-variation S states (step₁) (step)
  where step := markov/nnrat-kernel-step S states kernel (fun i => nnrat/right-residual-mass (left i) (right i))
  where step₁ := markov/nnrat-kernel-step S states kernel (fun i => nnrat/left-residual-mass (left i) (right i))
  where step₂ := markov/nnrat-kernel-step S states kernel right
  where step₃ := markov/nnrat-kernel-step S states kernel left

markov/nnrat-kernel-step-residual-expansion-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  → markov/nnrat-total-variation S states (step₁) (step) ≤ nnrat/map-sum S (fun target => nnrat/map-sum S (fun i => nnrat/distance ((fun i₁ => (fun i₂ => nnrat/left-residual-mass (left i₂) (right i₂)) i₁ · kernel i₁ target) i) ((fun i₁ => (fun i₂ => nnrat/right-residual-mass (left i₂) (right i₂)) i₁ · kernel i₁ target) i)) (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-residual-weighted-expansion-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (left right : S → ℚ≥0)
  → markov/nnrat-total-variation S states (step₁) (step) ≤ nnrat/map-sum S (fun target => nnrat/map-sum S (fun i => kernel i target · ((fun i₁ => nnrat/left-residual-mass (left i₁) (right i₁)) i + (fun i₁ => nnrat/right-residual-mass (left i₁) (right i₁)) i)) (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