Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-iteration

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_iteration.clj1 definitions, 6 theorems

Certified finite-horizon iteration of an exact NNRAT Markov kernel. `markov/nnrat-kernel-iterate` starts at an arbitrary mass and applies the kernel step once per natural-number successor. Pointwise equivalence is preserved through every horizon. For a normalized kernel, total mass is invariant and normalized initial masses remain normalized. Any stationary mass is pointwise invariant under every finite iterate. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-kernel-composition

markov/nnrat-kernel-iterate.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (x₁ : ℕ) (x₂ : S → ℚ≥0)
  (x₃ : S)
  → ℚ≥0

markov/nnrat-kernel-iterate-zero.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0) (state : S)
  → markov/nnrat-kernel-iterate S states kernel 0 mass state = mass state

markov/nnrat-kernel-iterate-successor.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (steps : ℕ) (mass : S → ℚ≥0)
  (target : S)
  → markov/nnrat-kernel-iterate S states kernel (data/succ steps) mass target = markov/nnrat-kernel-step S states kernel (fun state => iterate state) target
  where iterate := markov/nnrat-kernel-iterate S states kernel steps mass

markov/nnrat-kernel-iterate-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)
  (steps : ℕ) (state : S)
  → iterate left-mass state = iterate right-mass state
  where iterate := markov/nnrat-kernel-iterate S states kernel steps

markov/nnrat-kernel-iterate-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) (steps : ℕ)
  → probability/nnrat-total-mass S states (fun state => iterate state) = probability/nnrat-total-mass S states mass
  where iterate := markov/nnrat-kernel-iterate S states kernel steps mass

markov/nnrat-kernel-iterate-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)
  (steps : ℕ)
  → probability/nnrat-total-mass S states (fun state => iterate state) = 1
  where iterate := markov/nnrat-kernel-iterate S states kernel steps mass

markov/nnrat-stationary-kernel-iterate.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (fixed : markov/nnrat-stationary S states kernel mass) (steps : ℕ) (state : S)
  → markov/nnrat-kernel-iterate S states kernel steps mass state = mass state