Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-kernel-composition

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_kernel_composition.clj1 definitions, 5 theorems

Composition laws for exact finite NNRAT Markov kernels. The first kernel is applied before the second: (K ; L)(source,target) = sum_middle K(source,middle) * L(middle,target). Finite Fubini and distributivity prove both Chapman--Kolmogorov and exact preservation of total mass. Consequently normalized kernels are closed under composition, normalized masses remain normalized after every step, and a mass stationary for each factor is stationary for their composition. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-stationarity

markov/nnrat-kernel-compose.{u} :
  (S : Type u) (states : Finset S) (first-kernel second-kernel : S → S → ℚ≥0)
  (x₁ x₂ : S)
  → ℚ≥0

markov/nnrat-kernel-step-preserves-total-mass-equivalence.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  → probability/nnrat-total-mass S states (fun target => step target) = probability/nnrat-total-mass S states mass
  where step := markov/nnrat-kernel-step S states kernel mass

markov/nnrat-kernel-step-preserves-normalization.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (kernel-normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (mass-normalized : probability/nnrat-total-mass S states mass = 1)
  → probability/nnrat-total-mass S states (fun target => step target) = 1
  where step := markov/nnrat-kernel-step S states kernel mass

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

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

markov/nnrat-common-stationary-under-kernel-compose.{u} :
  (S : Type u) (states : Finset S) (first-kernel second-kernel : S → S → ℚ≥0)
  (mass : S → ℚ≥0) (first-fixed : markov/nnrat-stationary S states first-kernel mass)
  (second-fixed : markov/nnrat-stationary S states second-kernel mass)
  → markov/nnrat-stationary S states (fun source => fun target => compose source target) mass
  where compose := markov/nnrat-kernel-compose S states first-kernel second-kernel