Entropy rate of a stationary process #

For a stationary process p : StationaryProcess μ α on a finite alphabet α, the block entropy is H_n := H(X_0, …, X_{n-1}) and the entropy rate is H := lim_{n → ∞} H_n / n (Cover–Thomas). Existence of the limit is the principal content of this file.

The Birkhoff ergodic theorem and the Shannon–McMillan–Breiman theorem build on entropyRate defined here.

Main definitions #

• blockEntropy μ p n := entropy μ (p.blockRV n) — block entropy H(X_0, …, X_{n-1}).
• entropyRate μ p := Filter.atTop.limUnder (fun n => blockEntropy μ p n / n).
• conditionalEntropyTail μ p n := condEntropy μ (p.obs n) (p.blockRV n) — H(X_n | X_0, …, X_{n-1}).

Main statements #

• blockEntropy_succ_chain_rule — H_{n+1} = H_n + H(X_n | X_{<n}) (chain rule).
• blockEntropy_eq_sum_conditionalEntropyTail — iterated chain rule.
• blockEntropy_zero — H_0 = 0.
• conditionalEntropyTail_nonneg — 0 ≤ H(X_n | X_{<n}).
• conditionalEntropyTail_antitone — H(X_n | X_{<n}) non-increasing, from stationarity (joint pushforward equality via MeasurePreserving T)
  • conditioning monotonicity (condEntropy_le_condEntropy_of_pair).
• entropyRate_exists_of_stationary — blockEntropy / n converges: the antitone tail converges to some L, and Cesàro on the chain-rule decomposition gives blockEntropy / n → L.
• entropyRate_eq_lim_condEntropy — H(X_n | X_{<n}) → entropyRate, via Filter.Tendsto.limUnder_eq on the Cesàro convergence to identify entropyRate = L = lim tail.

Chain rule #

H_{n+1} = H_n + H(X_n | X_{<n}), the engine of the existence proof.

Antitonicity of conditionalEntropyTail #

H(X_{n+1} | X_0, …, X_n) ≤ H(X_n | X_0, …, X_{n-1}). Proof:

1. By stationarity (apply shift T), the joint pushforward μ.map (X_n, (X_0, …, X_{n-1})) equals μ.map (X_{n+1}, (X_1, …, X_n)), so the corresponding conditional entropies coincide (via condDistrib_map).
2. By conditioning monotonicity (condEntropy_le_condEntropy_of_pair), H(X_{n+1} | (X_0, (X_1, …, X_n))) ≤ H(X_{n+1} | (X_1, …, X_n)). The conditioner (X_0, (X_1, …, X_n)) reshapes to blockRV (n+1) via MeasurableEquiv.piFinSuccAbove ... 0 + prodComm.

Existence of the entropy rate #

We show Tendsto (blockEntropy μ p n / n) atTop (𝓝 H) for some H, by the following route:

• The chain rule gives blockEntropy μ p n = ∑_{i < n} conditionalEntropyTail μ p i.
• conditionalEntropyTail_antitone + non-negativity ⇒ tail converges to some L = ⨅ n, tail n.
• The Cesàro lemma Filter.Tendsto.cesaro converts Tendsto tail → Tendsto avg, and the chain-rule identity rewrites the Cesàro average as blockEntropy / n.

Equality with lim conditionalEntropyTail #

Tendsto (conditionalEntropyTail μ p) atTop (𝓝 (entropyRate μ p)).

Strategy: the chain rule + Cesàro gives blockEntropy / n → L = lim tail. The entropyRate is the limit of blockEntropy / n (Filter.limUnder of a convergent sequence equals the limit). The two limits agree by uniqueness.