Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-cesaro

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_cesaro.clj3 definitions, 8 theorems

Finite Cesaro occupation sums and averages for exact NNRAT Markov dynamics. Horizon n contains the n+1 masses mu, mu K, ..., mu K^n. The average takes an explicit exact weight; requiring count(n)*weight ~ 1 states precisely that the weight is the reciprocal sample count, without hiding a positivity side condition. A normalized kernel and mass give a normalized average, while a stationary mass is fixed by every finite Cesaro average. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-iteration

markov/nnrat-cesaro-count :
  (x₁ : ℕ)
  → ℚ≥0

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

markov/nnrat-cesaro-average.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (steps : ℕ) (mass : S → ℚ≥0)
  (weight : ℚ≥0) (x₁ : S)
  → ℚ≥0

markov/nnrat-cesaro-count-zero :
  → markov/nnrat-cesaro-count 0 = 1

markov/nnrat-cesaro-count-successor :
  (steps : ℕ)
  → markov/nnrat-cesaro-count (data/succ steps) = markov/nnrat-cesaro-count steps + 1

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

markov/nnrat-cesaro-sum-successor.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (steps : ℕ) (mass : S → ℚ≥0)
  (state : S)
  → markov/nnrat-cesaro-sum S states kernel (data/succ steps) mass state = markov/nnrat-cesaro-sum S states kernel steps mass state + markov/nnrat-kernel-iterate S states kernel (data/succ steps) mass state

markov/nnrat-cesaro-sum-total-mass.{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 => sum state) = markov/nnrat-cesaro-count steps
  where sum := markov/nnrat-cesaro-sum S states kernel steps mass

markov/nnrat-cesaro-average-normalized.{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 : ℕ) (weight : ℚ≥0)
  (weight-normalized : markov/nnrat-cesaro-count steps · weight = 1)
  → probability/nnrat-total-mass S states (fun state => average state) = 1
  where average := markov/nnrat-cesaro-average S states kernel steps mass weight

markov/nnrat-stationary-cesaro-sum.{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-cesaro-sum S states kernel steps mass state = markov/nnrat-cesaro-count steps · mass state

markov/nnrat-stationary-cesaro-average.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (mass : S → ℚ≥0)
  (fixed : markov/nnrat-stationary S states kernel mass) (steps : ℕ) (weight : ℚ≥0)
  (weight-normalized : markov/nnrat-cesaro-count steps · weight = 1)
  (state : S)
  → markov/nnrat-cesaro-average S states kernel steps mass weight state = mass state