Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-expectation-tower

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_expectation_tower.clj1 definitions, 2 theorems

The exact finite Markov expectation tower law over NNRAT. A kernel averages an observable backward while it pushes a mass forward. Finite Fubini proves these are adjoint operations: E_(mu K)[f] ~ E_mu[K f]. Combining this with stationarity proves E_mu[K f] ~ E_mu[f] for every observable. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-expectation-invariance

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

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

markov/nnrat-stationary-kernel-observable-expectation.{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)
  → expectation (fun source => observable source) = expectation observable
  where expectation := probability/nnrat-expectation S states mass
  where observable := markov/nnrat-kernel-observable S states kernel observable