Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-kernel-composition-positive

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_kernel_composition_positive.clj0 definitions, 2 theorems

Positive witnesses for finite exact-rational kernel composition. A listed intermediate with positive entries in both factor kernels witnesses a positive entry in their composition. The proof multiplies the two positive entries and retains that term through the finite sum. This is the algebraic path-concatenation rule for reachability. Native, kernel-checked, and axiom-free on D63.

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

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

markov/nnrat-kernel-compose-pointwise-positive.{u} :
  (S : Type u) (states : Finset S) (first-kernel second-kernel : S → S → ℚ≥0)
  (covered : ∀ (state : S), list/membership S (finset-data/enumeration S states) state)
  (first-positive : ∀ (left : S), ∀ (right : S), nnrat/positive (first-kernel left right))
  (second-positive : ∀ (left : S), ∀ (right : S), nnrat/positive (second-kernel left right))
  (source target : S)
  → nnrat/positive (markov/nnrat-kernel-compose S states first-kernel second-kernel source target)