InformationTheory

InformationTheory.Shannon.Stationary.Kernel

source

Imports 6

Stationary-process telescoping layer (LZ78 blockRV factorization) #

This file derives the algebraic telescoping backbone of the LZ78 per-path parsing factorization Pₙ{block ω} = ∏ⱼ condPhraseProb … (IsLZ78PerPathParsingFactorization, LZ78/ZivEntropyBridge.lean).

condPhraseProb μ p n ω j is defined as the ratio of successive parsing-prefix block probabilities prefixBlockProb ω (boundary (j+1)) / prefixBlockProb ω (boundary j). Over the phrase positions j ∈ range c this product telescopes to prefixBlockProb ω (boundary c) / prefixBlockProb ω (boundary 0) (Finset.prod_range_div). Since boundary 0 = 0 and the length-0 block has probability 1, the denominator is 1, leaving prefixBlockProb ω (boundary c).

The remaining content that connects this to Pₙ{block ω} is the parse-completeness fact boundary c = n (the parse consumes all n symbols) — together with the positivity of each ratio. These are the genuinely process-dependent inputs of the factorization; the telescoping algebra itself is unconditional and lives here.

theorem

InformationTheory.Shannon.parsingBoundary_zero

source
{α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) :
parsingBoundary μ p n ω 0 = 0

parsingBoundary μ p n ω 0 = 0: the empty parsing prefix consumes no symbols.

Used by
    theorem

    InformationTheory.Shannon.prefixBlockProb_zero

    source
    {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (ω : Ω) :
    prefixBlockProb μ p ω 0 = 1

    prefixBlockProb of the empty prefix is 1: Pₘ{block_m ω} at m = 0 is the probability of the unique length-0 block, which is 1.

    Used by
      theorem

      InformationTheory.Shannon.prod_condPhraseProb_telescope

      source
      {α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (c : ℕ) (hpos : ∀ j ≤ c, prefixBlockProb μ p ω (parsingBoundary μ p n ω j) ≠ 0) :
      ∏ j ∈ Finset.range c, condPhraseProb μ p n ω j = prefixBlockProb μ p ω (parsingBoundary μ p n ω c)

      Telescoping: the product of the per-phrase conditional probabilities over range c telescopes to prefixBlockProb ω (boundary c), using boundary 0 = 0 and prefixBlockProb ω 0 = 1.

      Proved by induction on c (a ℝ field telescoping, where the prod_range_div group lemma does not apply): each step cancels the denominator ratio against the previous prefix probability, which is nonzero by hpos.

      Used by

        Reduction of the factorization to parse-completeness + positivity #

        The telescoping above reduces the factor field of IsLZ78PerPathParsingFactorization to two genuinely process-dependent facts about the LZ78 parse: positivity of the intermediate prefix block probabilities, and parse-completeness boundary c = n (the parse consumes all n symbols). The latter is the load-bearing residual: the longest-prefix greedy parse lz78PhraseStrings leaves an unfinished tail (lz78PhraseStrings_total_length_le is ≤, not =), so boundary c = n is not unconditionally true for the present parse — it is the Cover–Thomas "last partial phrase" content.

        Ziv-direction factorization (parse-completeness defect fix) #

        The factor field of IsLZ78PerPathParsingFactorization (LZ78/ZivEntropyBridge.lean) was originally stated as the equality Pₙ{block ω} = ∏ⱼ condPhraseProb …. That equality is genuinely false in general: the longest-prefix greedy parse lz78PhraseStrings leaves an unfinished tail, so the phrase boundaries cover only boundary c ≤ n symbols (lz78PhraseStrings_total_length_le is ≤, not =), and the telescoping product equals prefixBlockProb ω (boundary c), which exceeds Pₙ = prefixBlockProb ω n whenever the parse is incomplete.

        The Ziv chain (Cover–Thomas) does not need that false equality — it needs only the inequality Pₙ{block ω} ≤ ∏ⱼ qⱼ (equivalently -log Pₙ ≥ ∑ⱼ -log qⱼ), which is unconditionally true: Pₙ = prefixBlockProb ω n ≤ prefixBlockProb ω (boundary c) = ∏ⱼ qⱼ by prefix monotonicity of the cylinder block probability (a shorter prefix has larger mass). The two ingredients below establish this, fixing the defect: the factorization is recast from a false equality to the true Ziv inequality. Positivity of the intermediate prefix block probabilities (a.s. regularity of the observed cylinders) is the only side condition.

        theorem

        InformationTheory.Shannon.prefixBlockProb_antitone

        source
        {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (ω : Ω) {m₁ m₂ : ℕ} (h : m₁ ≤ m₂) :
        prefixBlockProb μ p ω m₂ ≤ prefixBlockProb μ p ω m₁

        Prefix monotonicity of the block probability (unconditional): for m₁ ≤ m₂, the length-m₂ cylinder is contained in the length-m₁ cylinder (matching more coordinates is a stronger constraint), so its mass is smaller: prefixBlockProb ω m₂ ≤ prefixBlockProb ω m₁.

        This is the load-bearing measure-theoretic fact that turns the (false) factorization equality into the (true) Ziv inequality.

        Used by
          theorem

          InformationTheory.Shannon.parsingBoundary_complete_le

          source
          {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) :
          parsingBoundary μ p n ω (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length ≤ n

          The complete-phrase boundary never exceeds n: the total length of the emitted phrase strings is at most the input length (lz78PhraseStrings_total_length_le), so the parsing boundary at the full phrase count is ≤ n. This is the unconditional replacement for the false boundary c = n parse-completeness claim.

          Used by
            theorem

            InformationTheory.Shannon.blockProb_le_prod_condPhraseProb

            source
            {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (hpos : ∀ j ≤ (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length, prefixBlockProb μ p ω (parsingBoundary μ p n ω j) ≠ 0) :
            (MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω} ≤ ∏ j ∈ Finset.range (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length, condPhraseProb μ p n ω j

            Ziv-direction factorization inequality (parse-completeness defect fix): the block probability is bounded above by the product of the per-phrase conditional probabilities over the parse, Pₙ{block ω} ≤ ∏ⱼ condPhraseProb …. This is the true content the Ziv chain needs (replacing the false equality factor): the telescoping gives ∏ⱼ qⱼ = prefixBlockProb ω (boundary c) (prod_condPhraseProb_telescope), and prefix monotonicity (prefixBlockProb_antitone) gives Pₙ = prefixBlockProb ω n ≤ prefixBlockProb ω (boundary c) since boundary c ≤ n (parsingBoundary_complete_le).

            The only side condition is positivity of the intermediate prefix block probabilities (a.s. regularity of the observed cylinders) — not the false parse-completeness claim.

            Used by
              theorem

              InformationTheory.Shannon.parsingBoundary_le_n

              source
              {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (j : ℕ) :
              parsingBoundary μ p n ω j ≤ n

              The parsing boundary never exceeds n at any phrase index: the cumulative length of the first j phrases is bounded by the total phrase length, which is ≤ n. (For j ≥ c the prefix is the whole phrase list, so the boundary is constant = boundary c ≤ n.)

              Used by