InformationTheory

InformationTheory.Shannon.SMB.AlgoetCover.Liminf

source

Imports 11

SMB Algoet–Cover liminf direction and hypothesis-free capstone #

This file proves the liminf half of the Algoet–Cover sandwich and assembles the hypothesis-free Shannon–McMillan–Breiman theorem shannon_mcmillan_breiman.

References #

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

InformationTheory.Shannon.MRatioLowerZ_le_sq_eventually

source
{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) :
∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p, ∀ᶠ (n : ℕ) in Filter.atTop, MRatioLowerZ μ p n x ≤ ENNReal.ofReal (↑n ^ 2)

Borel–Cantelli consequence (Z-side): μZ-a.s., MRatioLowerZ n x ≤ n² eventually.

Used by
    theorem

    InformationTheory.Shannon.blockLogAvgZ_ge_negLogQInftyZ_minus_error

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) :
    ∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p, ∀ᶠ (n : ℕ) in Filter.atTop, negLogQInftyZ μ p n x / ↑n - 2 * Real.log ↑n / ↑n ≤ blockLogAvgZ μ p n x

    Logarithmic form (Z-side): μZ-a.s., eventually, blockLogAvgZ n x ≥ (1/n) · negLogQInftyZ n x - 2 log n / n.

    Used by
      theorem

      InformationTheory.Shannon.birkhoffAverage_pmfLogCondInfty_tendsto

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :
      ∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p.toStationaryProcess, Filter.Tendsto (fun (n : ℕ) => negLogQInftyZ μ p.toStationaryProcess n x / ↑n) Filter.atTop (nhds (entropyRate μ p.toStationaryProcess))

      Birkhoff for pmfLogCondInfty on the 2-sided side: applying Birkhoff to (μZ, shiftZ, pmfLogCondInfty), using ergodic_shiftZ, measurePreserving_shiftZ, integrable_pmfLogCondInfty, and integral_pmfLogCondInfty_eq_entropyRate.

      Used by
        theorem

        InformationTheory.Shannon.blockLogAvgZ_bddAbove_ae

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :
        ∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p.toStationaryProcess, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => blockLogAvgZ μ p.toStationaryProcess n x

        Z-side a.s. upper boundedness of blockLogAvgZ (transferred from the Ω-side blockLogAvg_bddAbove_ae, via the bridge blockLogAvgZ n (natExt ω) = blockLogAvg n ω and measurePreserving_forwardEmbed + μZ_nat_proj_eq).

        blockLogAvgZ n x depends only on natProj x : ℕ → α. We push the μ-a.s. statement Ω-blockLogAvg n ω bounded above through measurePreserving_forwardEmbed to a (μ.map forwardEmbed) = (μZ.map natProj)-a.s. statement on (ℕ → α), then pull back to μZ-a.s. on (ℤ → α) via natProj.

        Used by
          theorem

          InformationTheory.Shannon.liminf_blockLogAvgZ_ge_entropyRate

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :
          ∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p.toStationaryProcess, entropyRate μ p.toStationaryProcess ≤ Filter.liminf (fun (n : ℕ) => blockLogAvgZ μ p.toStationaryProcess n x) Filter.atTop

          Z-side liminf bound: μZ-a.s., liminf blockLogAvgZ n x ≥ entropyRate.

          Used by
            theorem

            InformationTheory.Shannon.algoet_cover_liminf_bound

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :
            ∀ᵐ (ω : Ω) ∂μ, entropyRate μ p.toStationaryProcess ≤ Filter.liminf (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop

            Final transfer to Ω-side: μ-a.s., entropyRate ≤ liminf blockLogAvg n ω.

            Bridge: blockLogAvgZ n x depends only on natProj x : ℕ → α. We transfer the Z-side a.s. liminf bound through natProj-forwardEmbed measure preservation to the Ω-side, using μZ_nat_proj_eq (= μ.map forwardEmbed) and the fact that blockLogAvgZ n (eN (forwardEmbed ω)) = blockLogAvg n ω where eN y i := y i.toNat is the trivial extension on ℤ.

            Used by

              D.7 — Main theorem (hypothesis-free assembly) #

              theorem

              InformationTheory.Shannon.shannon_mcmillan_breiman

              source
              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) :
              ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => blockLogAvg μ p.toStationaryProcess n ω) Filter.atTop (nhds (entropyRate μ p.toStationaryProcess))

              Shannon–McMillan–Breiman theorem: for a stationary ergodic process with finite alphabet α, the per-symbol negative log-likelihood blockLogAvg μ p n converges almost surely to the entropy rate entropyRate μ p.

              This is the hypothesis-free capstone: the four hypotheses of shannon_mcmillan_breiman_of_sandwich hold unconditionally for an ergodic process.

              See also algoet_cover_liminf_bound, algoet_cover_limsup_bound, blockLogAvg_bddAbove_ae, blockLogAvg_bddBelow_ae.

              Used by