Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-kernel-algebra

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

Congruence, associativity, and observable action for exact finite kernels. Kernel composition respects pointwise equivalence in both arguments and is associative up to NNRAT equivalence. Its backward action on observables composes in the same order: (K ; L)f ~ K(Lf). Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-expectation-tower

markov/nnrat-kernel-compose-respects-first-equivalence.{u} :
  (S : Type u) (states : Finset S) (left-first right-first : S → S → ℚ≥0)
  (same-first : ∀ (source : S), ∀ (target : S), left-first source target = right-first source target)
  (second-kernel : S → S → ℚ≥0) (source target : S)
  → markov/nnrat-kernel-compose S states left-first second-kernel source target = markov/nnrat-kernel-compose S states right-first second-kernel source target

markov/nnrat-kernel-compose-respects-second-equivalence.{u} :
  (S : Type u) (states : Finset S) (first-kernel left-second right-second : S → S → ℚ≥0)
  (same-second : ∀ (source : S), ∀ (target : S), left-second source target = right-second source target)
  (source target : S)
  → compose left-second source target = compose right-second source target
  where compose := markov/nnrat-kernel-compose S states first-kernel

markov/nnrat-kernel-compose-respects-equivalence.{u} :
  (S : Type u) (states : Finset S) (left-first right-first : S → S → ℚ≥0)
  (same-first : ∀ (source : S), ∀ (target : S), left-first source target = right-first source target)
  (left-second right-second : S → S → ℚ≥0)
  (same-second : ∀ (source : S), ∀ (target : S), left-second source target = right-second source target)
  (source target : S)
  → markov/nnrat-kernel-compose S states left-first left-second source target = markov/nnrat-kernel-compose S states right-first right-second source target

markov/nnrat-kernel-compose-associative.{u} :
  (S : Type u) (states : Finset S)
  (first-kernel second-kernel third-kernel : S → S → ℚ≥0) (source target : S)
  → markov/nnrat-kernel-compose S states (fun left => fun right => compose left right) third-kernel source target = markov/nnrat-kernel-compose S states first-kernel (fun left => fun right => compose₁ left right) source target
  where compose := markov/nnrat-kernel-compose S states first-kernel second-kernel
  where compose₁ := markov/nnrat-kernel-compose S states second-kernel third-kernel

markov/nnrat-kernel-observable-compose.{u} :
  (S : Type u) (states : Finset S) (first-kernel second-kernel : S → S → ℚ≥0)
  (observable : S → ℚ≥0) (source : S)
  → markov/nnrat-kernel-observable S states (fun left => fun right => compose left right) observable source = markov/nnrat-kernel-observable S states first-kernel (fun middle => observable middle) source
  where compose := markov/nnrat-kernel-compose S states first-kernel second-kernel
  where observable := markov/nnrat-kernel-observable S states second-kernel observable