InformationTheory

InformationTheory.Shannon.LZ78.ZivMeasureBridge

source

Imports 6

LZ78 length-grouping measure bridge — per-length sub-distribution + log-sum #

This file supplies the measure-theoretic + log-sum layer of the length-grouping route for the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (LZ78/AsymptoticOptimality/ParentBridgeAchievability.lean).

Approach #

ZivLengthGrouping.lean produced the abstract grouping inequality

c · log c ≤ ∑_ℓ c_ℓ · log c_ℓ + c · log D

(lz78PhraseStrings_card_mul_log_le_sum_length_group), fibering the distinct LZ78 phrases by List.length (c = #phrases, c_ℓ = #{phrases of length ℓ}, D = #distinct lengths). This file converts the inner c_ℓ · log c_ℓ terms into negative-log marginal probabilities and aggregates:

  1. Per-length sub-distribution (sum_marginal_real_le_one): for the length-ℓ marginal P_ℓ(Z) = (μ.map (blockRV ℓ)).real {Z} and a finite set S of distinct strings Z : Fin ℓ → α, ∑_{Z ∈ S} P_ℓ(Z) ≤ 1. This is a pure probability fact: distinct singletons are disjoint, so the sum is the measure of the finset, bounded by the measure of the whole space.

  2. Per-length log-sum step (group_card_mul_log_le_sum_neg_log): applying log_sum_inequality (ZivEntropyBridge.lean) with aᵢ ≡ 1, bᵢ = P_ℓ(Zᵢ) over a group S of card S distinct strings with ∑ P ≤ 1 and P > 0 gives card S · log (card S) ≤ ∑_{Z ∈ S} -log P_ℓ(Z).

  3. Aggregation (lz78PhraseStrings_mul_log_le_sum_neg_log_marginal_add_overhead): combine the grouping inequality with step 2 applied per length group, instantiating P_ℓ at the actual phrase marginals via the injection w ↦ (w[·]) : List α → (Fin ℓ → α) (injective on length-ℓ lists), giving

    c · log c ≤ ∑_{phrases w} -log P_{|w|}(w) + c · log D.

What step 3 does not supply is the link from the marginal sum ∑_w -log P_{|w|}(w) to the joint -log Pₙ = n · blockLogAvg with an o(n) slack: the per-phrase marginals ignore the dependence between successive phrases, so for a source with memory ∑_w -log P_{|w|}(w) ≥ -log Pₙ, the opposite of the direction the Ziv chain needs. ziv_aseventual_le_blockLogAvg₂ is therefore reached through the conditional per-k-state route (ZivCondGrouping.lean), whose chain rule reaches -log Pₙ exactly.

Step 1 — per-length sub-distribution #

theorem

InformationTheory.Shannon.sum_marginal_real_le_one

source
{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (ℓ : ℕ) (S : Finset (Fin ℓ → α)) :
∑ Z ∈ S, (MeasureTheory.Measure.map (p.blockRV ℓ) μ).real {Z} ≤ 1

For the length-ℓ marginal P_ℓ(Z) = (μ.map (blockRV ℓ)).real {Z} and any finite set S of distinct strings Z : Fin ℓ → α, the marginal masses sum to at most 1.

Pure probability fact: distinct singletons are pairwise disjoint, so the sum equals the marginal measure of S (sum_measureReal_singleton), bounded by the total mass 1 of the pushed-forward probability measure (measureReal_le_one).

Used by

    Step 2 — per-length log-sum step #

    theorem

    InformationTheory.Shannon.group_card_mul_log_le_sum_neg_log

    source
    {α : Type u_1} {ℓ : ℕ} (S : Finset (Fin ℓ → α)) (P : (Fin ℓ → α) → ℝ) (hPpos : ∀ Z ∈ S, 0 < P Z) (hPsum : ∑ Z ∈ S, P Z ≤ 1) :
    ↑S.card * Real.log ↑S.card ≤ ∑ Z ∈ S, -Real.log (P Z)

    The per-length log-sum step: for a finite group S of distinct strings Z : Fin ℓ → α with strictly positive marginals P_ℓ(Z) > 0 whose masses sum to at most 1,

    card S · log (card S) ≤ ∑_{Z ∈ S} -log P_ℓ(Z).

    log_sum_inequality with aᵢ ≡ 1, bᵢ = P_ℓ(Zᵢ): the LHS becomes card S · log (card S / ∑ P) and ∑ P ≤ 1 makes the -log (∑ P) ≥ 0 correction only help.

    Used by

      Step 3 — aggregation over phrases #

      noncomputable def

      InformationTheory.Shannon.toFinVec

      source
      {α : Type u_1} [Nonempty α] (ℓ : ℕ) (w : List α) :
      Fin ℓ → α

      Read the first ℓ entries of a list into a Fin ℓ → α function, defaulting past the end. Injective on length-ℓ lists.

      Equations
      Instances For
        Used by
          theorem

          InformationTheory.Shannon.toFinVec_injOn

          source
          {α : Type u_1} [Nonempty α] (ℓ : ℕ) :
          Set.InjOn (toFinVec ℓ) {w : List α | w.length = ℓ}
          Used by
            theorem

            InformationTheory.Shannon.lz78PhraseStrings_mul_log_le_sum_neg_log_marginal_add_overhead

            source
            {α : Type u_1} {Ω : Type u_2} [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (input : List α) (hpos : ∀ w ∈ (lz78PhraseStrings input).toFinset, 0 < (MeasureTheory.Measure.map (p.blockRV w.length) μ).real {toFinVec w.length w}) :
            have phrases := (lz78PhraseStrings input).toFinset; ↑(lz78PhraseStrings input).length * Real.log ↑(lz78PhraseStrings input).length ≤ ∑ w ∈ phrases, -Real.log ((MeasureTheory.Measure.map (p.blockRV w.length) μ).real {toFinVec w.length w}) + ↑(lz78PhraseStrings input).length * Real.log ↑(Finset.image List.length phrases).card

            The length-grouped marginal entropy bound for the LZ78 phrase set.

            Instantiating the abstract grouping inequality at the actual length-ℓ marginals, with c = #phrases, D = #distinct lengths:

            c · log c ≤ ∑_{phrases w} -log P_{|w|}(w) + c · log D,

            where P_{|w|}(w) = (μ.map (blockRV |w|)).real {toFinVec |w| w} is the marginal mass of the cylinder of the string w (read as a Fin |w| → α vector). The positivity P_{|w|}(w) > 0 over the (a.s.) observed phrases is a regularity precondition.

            The sub-distribution hypothesis is discharged from step 1 (sum_marginal_real_le_one) via the length-fiber injection toFinVec; the positivity is the only precondition.

            Used by