Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-stationarity

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_stationarity.clj4 definitions, 5 theorems

Exact finite NNRAT Markov kernels, detailed balance, and stationarity. `markov/nnrat-kernel-step` pushes a mass function through a finite kernel. Kernel normalization is rowwise total mass one. Detailed balance equates every directed probability flow with its reverse. Summing those checked pairwise equivalences and factoring the target mass proves stationarity. The module also gives pointwise congruence of the step in both its mass and kernel arguments, and proves that a stationary normalized mass remains normalized after a step. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-value-optimality

markov/nnrat-kernel-step.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0) (x₁ : S)
  → ℚ≥0

markov/nnrat-kernel-rows-normalized.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  → Prop

markov/nnrat-detailed-balance.{u} :
  (S : Type u) (mass : S → ℚ≥0) (kernel : S → S → ℚ≥0)
  → Prop

markov/nnrat-stationary.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  → Prop

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

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

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

markov/nnrat-detailed-balance-implies-stationary.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (balanced : markov/nnrat-detailed-balance S mass kernel)
  → markov/nnrat-stationary S states kernel mass

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