InformationTheory.Shannon.SMB.McMillanBreiman

Imports 6

Shannon-McMillan-Breiman theorem (sandwich form) #

Cover–Thomas: for a stationary ergodic process with finite alphabet α, the per-symbol negative log-likelihood

-(1/n) log P(X_0, …, X_{n-1})

converges almost surely to the entropy rate H. This file packages the sandwich form of the conclusion: assuming liminf ≥ H and limsup ≤ H almost surely (the two halves of the Cover–Thomas bound which Birkhoff supplies), we deduce a.s. convergence via tendsto_of_le_liminf_of_limsup_le.

The hypothesis-free capstone shannon_mcmillan_breiman lives in InformationTheory.Shannon.SMBAlgoetCover: it discharges the two sandwich inequalities and a.s. boundedness unconditionally via the Algoet–Cover bounds (algoet_cover_liminf_bound / algoet_cover_limsup_bound), which rest on the Birkhoff ergodic theorem (BirkhoffErgodic), the two-sided projective-limit construction (Probability.TwoSidedExtension), and backward-martingale convergence.

We also publish the expected-value level statement, which does not need Birkhoff.

Main definitions #

blockLogAvg μ p n ω — -(1/n) * log P_n({block_n ω}), the per-block empirical entropy estimator for the observed sample.

Main statements #

shannon_mcmillan_breiman_of_sandwich — sandwich version: from the two Cover–Thomas inequalities (liminf ≥ H, limsup ≤ H) plus a.s. boundedness, derive Tendsto blockLogAvg n → H a.s.
expected_blockLogAvg_eq — 𝔼[blockLogAvg μ p n] = blockEntropy μ p n / n.
tendsto_expected_blockLogAvg — the expected-value SMB: 𝔼[blockLogAvg μ p n] → entropyRate μ p as n → ∞.

noncomputable def

InformationTheory.Shannon.blockLogAvg

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) :

Ω → ℝ

Per-block negative log-likelihood average for the observed sample.

blockLogAvg μ p n ω := -(1/n) * log P_n({block_n ω}) where P_n = μ.map (blockRV n). Cover–Thomas calls this -(1/n) log p(X^n).

For n = 0 the value is 0 (multiplication by 1/0 = 0); only n > 0 behavior is informative.

Equations

InformationTheory.Shannon.blockLogAvg μ p n ω = -(1 / ↑n) * Real.log ((MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω})

Instances For

Used by

theorem

InformationTheory.Shannon.measurable_blockLogAvg

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) :

Measurable (blockLogAvg μ p n)

Measurability of blockLogAvg μ p n.

Used by

Sandwich form (Cover–Thomas) #

theorem

InformationTheory.Shannon.shannon_mcmillan_breiman_of_sandwich

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) (h_liminf : ∀ᵐ (ω : Ω) ∂μ, entropyRate μ p.toStationaryProcess ≤ Filter.liminf (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop) (h_limsup : ∀ᵐ (ω : Ω) ∂μ, Filter.limsup (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop ≤ entropyRate μ p.toStationaryProcess) (h_bdd_above : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) (h_bdd_below : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop (nhds (entropyRate μ p.toStationaryProcess))

Shannon–McMillan–Breiman theorem (sandwich form): if the per-symbol log-likelihood average blockLogAvg μ p n satisfies the two sandwich bounds (liminf ≥ entropy rate, limsup ≤ entropy rate) and is a.s. bounded, then it converges to the entropy rate a.s.

Used by

Expected-value level (no Birkhoff needed) #

theorem

InformationTheory.Shannon.expected_blockLogAvg_eq

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) {n : ℕ} (hn : 0 < n) :

∫ (ω : Ω), blockLogAvg μ p n ω ∂μ = blockEntropy μ p n / ↑n

The expected per-symbol negative log-likelihood equals blockEntropy / n.

This is the discrete-alphabet analogue of integral_logLikelihood_zero in AEP/Basic/Core.lean: push forward via blockRV n, collapse the integral over a finite alphabet to a sum, and recognize the resulting sum as the entropy times -(1/n).

Used by