InformationTheory.Shannon.SMB.AlgoetCover.Boundedness
D.6 — Boundedness (hoisted before D.5 because the liminf transfer uses #
blockLogAvg_bddAbove_ae to establish μZ-a.s. upper boundedness of blockLogAvgZ).
InformationTheory.Shannon.blockLogAvg_bddAbove_ae
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(p : ErgodicProcess μ α)
:
∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω
A.s. boundedness above for blockLogAvg.
A.s., blockLogAvg ≤ negLogQk(k=0)/n + 2·log n / n (from
blockLogAvg_le_negLogQk_plus_error), and the RHS converges a.s. to
conditionalEntropyTail μ p 0 (finite), hence the RHS is eventually bounded
above and so is blockLogAvg.
Used by
InformationTheory.Shannon.blockLogAvg_bddBelow_ae
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(p : ErgodicProcess μ α)
:
∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω
A.s. boundedness below for blockLogAvg.