Skip to content

InformationTheory.Shannon.SMB.AlgoetCover.Limsup

Imports 11

D.4 — limsup direction #

theorem

InformationTheory.Shannon.blockLogAvg_le_negLogQk_plus_error

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

∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop , blockLogAvg μ p n ω ≤ negLogQk μ p k n ω / ↑n + 2 * Real.log ↑n / ↑n

Logarithmic form of MRatioUp_le_sq_eventually: pointwise blockLogAvg upper bound by the k-Markov approximation plus a 2 log n / n error.

Used by

theorem

InformationTheory.Shannon.limsup_blockLogAvg_le_condEntropyTail

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) (k : ℕ) :

∀ᵐ (ω : Ω) ∂μ, Filter.limsup (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop ≤ conditionalEntropyTail μ p.toStationaryProcess k

Per-k limsup bound: limsup blockLogAvg ≤ conditionalEntropyTail μ p k a.s.

Used by

theorem

InformationTheory.Shannon.algoet_cover_limsup_bound

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :

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

Algoet–Cover limsup bound: limsup blockLogAvg ≤ entropyRate μ p a.s.

Used by