Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-expectation-invariance

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_expectation_invariance.clj0 definitions, 3 theorems

Exact observable invariance under stationary finite Markov dynamics. A stationary NNRAT mass gives the same finite expectation before and after one kernel step, after every finite iterate, and under every correctly normalized finite Cesaro occupation average. These theorems connect the MCMC distribution laws to the reusable finite-expectation interface. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-cesaro

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

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

markov/nnrat-stationary-cesaro-expectation-invariant.{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)
  (observable : S → ℚ≥0)
  → probability/nnrat-expectation S states (fun state => average state) observable = probability/nnrat-expectation S states mass observable
  where average := markov/nnrat-cesaro-average S states kernel steps mass weight