InformationTheory

InformationTheory.Shannon.LZ78.ZivAchievabilityComposition

source

Imports 4

LZ78 achievability composition: threading + (k-state, length) grouping #

This file composes the two upstream bricks of the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (LZ78/AsymptoticOptimality/ParentBridgeAchievability.lean):

  • negLogQk_parse_threading (ZivThreading.lean): the a.s. threading identity negLogQk μ p k n ω = (leading boundary) + (per-phrase sum) + (trailing tail), where the per-phrase sum is position-indexed (∑ j : Fin c).
  • condState_grouping_bound_mean (ZivCondGrouping.lean): the (k-state, length) grouped entropy bound with o(n) mean-length overhead, on a Finset (List α) of distinct phrase strings.

The composition target is the a.s. lower bound c · log c ≤ negLogQk + overhead in the manifestly-o(n) mean-length form, the input to the downstream "divide by n, limsup, diagonalize k → ∞" step.

Two sub-steps #

  • (A) boundary-nonneg. The threading identity carries two boundary sums of pmfLogCondMarkov μ p k i ω. Since pmfLogCondMarkov is -log of a conditional kernel singleton mass ≤ 1 (the kernel is a Markov kernel, so its value at every point is a probability measure), each term is ≥ 0, hence the per-phrase sum is ≤ negLogQk. This holds unconditionally (no a.s. caveat needed for the positivity).
  • (B) reindex Fin c → Finset + apply condState_grouping_bound_mean. The threading phrase sum is position-indexed; condState_grouping_bound_mean consumes a Finset (List α) of distinct phrase strings. Bridging the two requires the c tiled phrases to be distinct as strings (so card = c) and the content/state correspondence between the position-indexed terms and the string-indexed terms. This is now discharged (sorryAx-free): the slice/content correspondence flatten_drop_take_getElem (threaded through the tiling chain) identifies the j-th tiled slice with the (bAbsorbed + j)-th greedy phrase, lz78PhraseStrings_nodup gives distinctness (card = c), and the per-term reindex composes via Finset.sum_image.

Telescoping helper #

theorem

InformationTheory.Shannon.sum_range_consecutive_sub_of_monotone

source
(M : ℕ → ℕ) (hMmono : ∀ (i : ℕ), M i ≤ M (i + 1)) (c : ℕ) :
∑ j ∈ Finset.range c, (M (j + 1) - M j) = M c - M 0

Telescoping of consecutive differences of a monotone ℕ → ℕ sequence: ∑_{j<c} (M (j+1) - M j) = M c - M 0.

Used by

    Sub-step (A): nonnegativity of the per-step Markov log-likelihood #

    theorem

    InformationTheory.Shannon.pmfLogCondMarkov_nonneg

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

    The per-step k-Markov negative conditional log-likelihood is nonnegative: pmfLogCondMarkov μ p k i ω = -log m where m = (condDistrib … ).real {…} is a singleton mass of a probability measure (condDistrib is a Markov kernel), hence 0 ≤ m ≤ 1 and -log m ≥ 0. Holds for every ω (no a.s. caveat).

    Used by

      Sub-step (A): the per-phrase sum is bounded by negLogQk #

      theorem

      InformationTheory.Shannon.phraseSum_le_negLogQk

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k n : ℕ) (ω : Ω) (b c e : ℕ) (N : Fin (c + 1) → ℕ) (hthread : negLogQk μ p k n ω = ∑ i ∈ Finset.range b, pmfLogCondMarkov μ p k i ω + ∑ j : Fin c, -Real.log (condQkState μ p k (windowState p k (N j.castSucc) ω) (N j.succ - N j.castSucc) fun (m : Fin (N j.succ - N j.castSucc)) => p.obs (N j.castSucc + ↑m) ω).toReal + ∑ i ∈ Finset.Ico e n, pmfLogCondMarkov μ p k i ω) :
      ∑ j : Fin c, -Real.log (condQkState μ p k (windowState p k (N j.castSucc) ω) (N j.succ - N j.castSucc) fun (m : Fin (N j.succ - N j.castSucc)) => p.obs (N j.castSucc + ↑m) ω).toReal ≤ negLogQk μ p k n ω

      The position-indexed per-phrase sum from the threading identity is bounded above by negLogQk, because the two boundary sums (pmfLogCondMarkov over [0,b) and [e,n)) are nonnegative. Stated abstractly in the shape produced by negLogQk_parse_threading.

      Used by
        theorem

        InformationTheory.Shannon.condQkState_congr_length

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (s : Fin k → α) (ℓ₁ ℓ₂ : ℕ) (hℓ : ℓ₁ = ℓ₂) (Z₁ : Fin ℓ₁ → α) (Z₂ : Fin ℓ₂ → α) (hZ : ∀ (i : Fin ℓ₁), Z₁ i = Z₂ (Fin.cast hℓ i)) :
        condQkState μ p k s ℓ₁ Z₁ = condQkState μ p k s ℓ₂ Z₂

        Congruence for condQkState under a length equality: equal state s, equal lengths (ℓ₁ = ℓ₂), and continuations equal after the Fin.cast give equal masses. Used to bridge the (phrase j).length-indexed term to the N j.succ - N j.castSucc-indexed threading term.

        Used by
          theorem

          InformationTheory.Shannon.parseTiling_totalLength_le

          source
          (c e n b : ℕ) (N : Fin (c + 1) → ℕ) (hNb : N 0 = b) (hNe : N (Fin.last c) = e) (hen : e ≤ n) (hmono : ∀ (j : Fin c), N j.castSucc + 1 ≤ N j.succ) :
          ∑ j : Fin c, (N j.succ - N j.castSucc) ≤ n
          Used by
            theorem

            InformationTheory.Shannon.parseTiling_phrase_slice_injective

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [DecidableEq α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (c e bAbsorbed : ℕ) (N : Fin (c + 1) → ℕ) (hNe : N (Fin.last c) = e) (hen : e ≤ n) (hmono : ∀ (j : Fin c), N j.castSucc + 1 ≤ N j.succ) (hslice : ∀ (j : Fin c), (lz78PhraseStrings (List.ofFn fun (i : Fin n) => p.blockRV n ω i))[bAbsorbed + ↑j]? = some (List.take (N j.succ - N j.castSucc) (List.drop (N j.castSucc) (List.ofFn fun (i : Fin n) => p.blockRV n ω i)))) :
            (∀ (j : Fin c), (List.take (N j.succ - N j.castSucc) (List.drop (N j.castSucc) (List.ofFn fun (i : Fin n) => p.blockRV n ω i))).length = N j.succ - N j.castSucc) ∧ (∀ (j : Fin c), ∀ m < N j.succ - N j.castSucc, (List.take (N j.succ - N j.castSucc) (List.drop (N j.castSucc) (List.ofFn fun (i : Fin n) => p.blockRV n ω i)))[m]? = some (p.obs (N j.castSucc + m) ω)) ∧ Function.Injective fun (j : Fin c) => List.take (N j.succ - N j.castSucc) (List.drop (N j.castSucc) (List.ofFn fun (i : Fin n) => p.blockRV n ω i))
            Used by

              Sub-step (B): the achievability composition lemma #

              theorem

              InformationTheory.Shannon.ziv_achievability_composition

              source
              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k n : ℕ) :
              ∀ᵐ (ω : Ω) ∂μ, ∃ (c : ℕ) (bAbsorbed : ℕ) (Ntot : ℕ), c + bAbsorbed = (lz78PhraseStrings (List.ofFn fun (i : Fin n) => p.blockRV n ω i)).length ∧ bAbsorbed ≤ k + 1 ∧ Ntot ≤ n ∧ ↑c * Real.log ↑c ≤ negLogQk μ p k n ω + (↑c * Real.log (↑Ntot / ↑c) + ↑c + ↑c * Real.log ↑(Fintype.card α ^ k))

              The LZ78 achievability composition (a.s. form): for a.e. ω, the tiled phrase count c and total parsed length Ntot ≤ n satisfy the o(n)-overhead Ziv lower bound c · log c ≤ negLogQk μ p k n ω + (c · log (Ntot / c) + c + c · log (#states)), with the phrase count c anchored to the genuine distinct-phrase count of the parse (c + bAbsorbed = (lz78PhraseStrings …).length, bAbsorbed ≤ k+1).

              This is the input to the downstream "divide by n, limsup, diagonalize k → ∞" step: divide by n, the overhead is o(n) (mean length ~ log n, c = O(n/log n)), and the boundary terms vanish.

              Now genuinely closed (sorryAx-free). The former residual was the (B) reindexing bridge from the position-indexed threading sum (∑ j : Fin c) onto the distinct-phrase Finset consumed by condState_grouping_bound_mean. It is discharged by:

              • the slice/content correspondence flatten_drop_take_getElem (GreedyLongestPrefix.lean, sorryAx-free) threaded through the tiling chain (lz78_parse_tiling_positions → lz78_block_tiling → negLogQk_parse_threading), which exposes that the j-th tiled slice is the (bAbsorbed + j)-th greedy phrase string;
              • the distinctness of those slices via lz78PhraseStrings_nodup (so the image Finset has card = c);
              • the per-term reindex condQkState (windowState …) (…) (fun m => p.obs …) ↦ condQkState (st w) |w| (toFinVec |w| w) with st the trailing k-state read off the parse inverse, plus the per-phrase positivity condQkState_pos_of_markovFactor_pos.

              The c = 0 boundary degenerates honestly to 0 ≤ 0. The rest of the achievability argument — the variable-depth length-grouping AEP and the limsup discharge connecting to entropyRate₂ — lives downstream at ziv_aseventual_le_blockLogAvg₂ / lz78Greedy_achievability_ae, not in this brick (c·log c ≤ negLogQk + o(n)).

              @audit:ok (non-circular, non-bundled: conclusion is the unchanged inequality (c·log c ≤ negLogQk + (c·log(Ntot/c) + c + c·log((card α)^k))), no input hypothesis added. The two sub-bounds are PROVEN (hA = phraseSum_le_negLogQk, hB from the genuine reindex onto the distinct-phrase Finset + condState_grouping_bound_mean), combined by linarith — sufficiency holds, nothing is asserted as a hypothesis. Non-vacuous: the phrase count c is anchored to the parse by c + bAbsorbed = (lz78PhraseStrings …).length with bAbsorbed ≤ k + 1, so the existential cannot escape through c = 0 for a long block).

              Used by