Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-positive-step

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

Positive support propagation through a finite exact-rational kernel. If a listed source has positive current mass and a positive transition to a target, then one kernel step has positive mass at that target. Other source contributions are merely nonnegative and cannot destroy the witness. This is the reusable induction step for finite positive paths and reachability. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.map-sum-positive

markov/nnrat-kernel-step-positive-of-member.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (source target : S)
  (source-member : list/membership S (finset-data/enumeration S states) source)
  (source-positive : nnrat/positive (mass source))
  (edge-positive : nnrat/positive (kernel source target))
  → nnrat/positive (markov/nnrat-kernel-step S states kernel mass target)

markov/nnrat-kernel-iterate-positive-successor-of-member.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0) (steps : ℕ)
  (middle target : S)
  (middle-member : list/membership S (finset-data/enumeration S states) middle)
  (middle-positive : nnrat/positive (iterate steps mass middle))
  (edge-positive : nnrat/positive (kernel middle target))
  → nnrat/positive (iterate (data/succ steps) mass target)
  where iterate := markov/nnrat-kernel-iterate S states kernel

markov/nnrat-kernel-iterate-positive-along-trajectory.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (trajectory : ℕ → S)
  (trajectory-member : ∀ (step : ℕ), list/membership S (finset-data/enumeration S states) (trajectory step))
  (edge-positive : ∀ (step : ℕ), nnrat/positive (kernel (trajectory step) (trajectory (data/succ step))))
  (initial-positive : nnrat/positive (mass (trajectory 0))) (steps : ℕ)
  → nnrat/positive (markov/nnrat-kernel-iterate S states kernel steps mass (trajectory steps))