SMB chain rule decomposition #

For a stationary process p : StationaryProcess μ α over a finite alphabet, this file establishes the Cover–Thomas chain rule for log-likelihood:

-log P_n({block_n ω}) = ∑_{i<n} -log P(obs i | block_i)(block_i ω){obs i ω}

a.s. over ω. The right-hand side is named pmfLogCond μ p i ω. The result is the algebraic identity that the Levy convergence and the Birkhoff + Cesàro sandwich use to discharge the four hypotheses of shannon_mcmillan_breiman_of_sandwich.

Main definitions #

• pmfLogCond μ p i ω — per-step conditional negative log-likelihood -log (condDistrib (obs i) (blockRV i) μ (block_i ω)).real {obs i ω}.

Main statements #

• block_measure_succ_singleton_eq — multiplicative ENNReal chain rule at singletons: P_{n+1}({block_{n+1} ω}) = P_n({block_n ω}) · c_n(...){obs n ω}.
• block_singleton_pos_ae_at — a.s. positivity of P_n({block_n ω}) for each n.
• log_block_eq_sum_pmfLogCond — a.s. log identity (chain rule): -log P_n({block_n ω}) = ∑_{i<n} pmfLogCond μ p i ω.

References #

• T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Per-step conditional log-likelihood #

Multiplicative chain rule at singletons (ENNReal level) #

A.s. positivity of P_n({block_n ω}) #

Conditional singleton positivity (consequence of block positivity) #

Integrability and integral identity #

pmfLogCond μ p l is integrable, and its integral equals conditionalEntropyTail μ p l. This bridges the Birkhoff time-average to the spatial average used by the sandwich.

Birkhoff per-level application #

For each fixed level l, the Birkhoff time average of pmfLogCond p l along the orbit converges a.s. to conditionalEntropyTail μ p l. This is the "l-Markov approximation" output that the SMB sandwich (Algoet–Cover) chains with H_l → entropyRate to obtain the full result.