Stationary processes #

Lean encoding of a stationary (resp. ergodic) discrete-time process via a MeasurePreserving (resp. Ergodic) shift T : Ω → Ω together with a single observable X : Ω → α. Time-i observation is X ∘ T^[i], the block (X_0, …, X_{n-1}) is blockRV n : Ω → (Fin n → α).

These definitions are the foundation for the entropy rate, Birkhoff's ergodic theorem, the log-likelihood chain rule, and the Shannon–McMillan–Breiman theorem.

Main definitions #

• StationaryProcess — bundles T, X, MeasurePreserving T μ μ, Measurable X.
• StationaryProcess.obs i — the time-i observation X ∘ T^[i].
• StationaryProcess.blockRV n — joint (X_0, …, X_{n-1}) : Ω → (Fin n → α).
• ErgodicProcess — extends StationaryProcess with Ergodic T μ.

Main statements #

• StationaryProcess.measurable_obs — each obs i is measurable.
• StationaryProcess.measurable_blockRV — blockRV n is measurable.
• StationaryProcess.identDistrib_obs_zero — obs i has the same law as obs 0 (stationarity, derived from MeasurePreserving.iterate).