InformationTheory

InformationTheory.Shannon.LZ78.PhraseCounting

source

Imports 11

LZ78 distinct-phrase counting bound — c · log c ≤ K·n #

InformationTheory/Shannon/LZ78/GreedyLongestPrefix.lean establishes the longest-prefix greedy parse lz78PhraseStrings together with its distinct invariant lz78PhraseStrings_nodup and the total-length conservation lz78PhraseStrings_total_length_le.

This file supplies the Cover–Thomas counting bound as a combinatorial inequality on any Nodup list of non-empty strings over a finite alphabet:

c · log c ≤ K · T          (K = 4·log(|α|+1),  T = total symbol count)

which, instantiated at lz78PhraseStrings input with T ≤ input.length, gives the Ziv product bound c(n) · log c(n) ≤ K·n (★). Composed with the inversion isBigO_natCast_div_log_of_mul_log_le (LZ78/PhraseCountAsymptotics.lean), this yields c(n) = O(n / log n).

Approach #

The substantive content is the shortest-first packing lower bound on the total length T of c distinct non-empty strings. Two ingredients:

  1. Geometric stratification (card_short_le) — the number of distinct strings of length ≤ L is at most (b+1)^(L+1), where b = |α|. Proof: w ↦ (fun i : Fin (L+1) => w[i]?) is injective on strings of length ≤ L (two such strings agreeing on indices 0..L of getElem? are equal — indices past their length both return none), so List.Nodup.length_le_card into Fin (L+1) → Option α (card (b+1)^(L+1)) bounds the count.

  2. Packing (total_length_ge) — among c distinct strings, at most (b+1)^(L+1) are short (length ≤ L), so at least c - (b+1)^(L+1) are long (length ≥ L+1), each contributing ≥ L+1 to T. Choosing the threshold L+1 = Nat.log (b+1) c - 1 makes the short count ≤ c/2, giving T ≥ (L+1)·(c/2) ≈ (c/2)·log_{b+1} c.

The real-analysis assembly converts Nat.log (b+1) c to Real.log c / Real.log (b+1) via Nat.pow_log_le_self / Nat.lt_pow_succ_log_self, yielding c·log c ≤ 4·log(b+1)·T.

File layout #

§1. Strings as Option-tuples (injection for stratification) #

def

InformationTheory.Shannon.toOptTuple

source
{α : Type u_1} (L : ℕ) (w : List α) :
Fin (L + 1) → Option α

Inject length-≤L strings into Fin (L+1) → Option α by recording each of the first L+1 getElem? slots.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.toOptTuple_injOn

      source
      {α : Type u_1} (L : ℕ) :
      Set.InjOn (toOptTuple L) {w : List α | w.length ≤ L}

      Two strings of length ≤ L with the same getElem? on indices 0..L are equal.

      Used by

        §2. Geometric stratification #

        theorem

        InformationTheory.Shannon.card_short_le

        source
        {α : Type u_1} [Fintype α] {L : ℕ} (ws : List (List α)) (hnodup : ws.Nodup) (hlen : ∀ w ∈ ws, w.length ≤ L) :
        ws.length ≤ (Fintype.card α + 1) ^ (L + 1)

        A Nodup list of strings, all of length ≤ L, has length at most (|α|+1)^(L+1).

        Used by

          §3. Shortest-first packing #

          theorem

          InformationTheory.Shannon.packing_nat

          source
          {α : Type u_1} [Fintype α] [Nonempty α] (ws : List (List α)) (hnodup : ws.Nodup) (L : ℕ) :
          (L + 1) * (ws.length - (Fintype.card α + 1) ^ (L + 1)) ≤ (List.map List.length ws).sum

          For any threshold L, the total length T of a Nodup string list dominates (L+1) times the number of long strings (length > L), and the long-string count is c minus the short count, which is bounded by (b+1)^(L+1). Concretely (L+1)·(c - (b+1)^(L+1)) ≤ T.

          Used by
            theorem

            InformationTheory.Shannon.total_length_ge_count_mul_log

            source
            {α : Type u_1} [Fintype α] [Nonempty α] (ws : List (List α)) (hnodup : ws.Nodup) (hne : ∀ w ∈ ws, w ≠ []) :
            ↑ws.length * Real.log ↑ws.length ≤ 8 * Real.log (↑(Fintype.card α) + 1) * ↑(List.map List.length ws).sum

            The total-length lower bound at the core of the Cover–Thomas packing argument: a Nodup list of non-empty strings with c = ws.length and total length T = Σ lengths satisfies c · log c ≤ K · T with K = 4·log(|α|+1).

            Used by

              §4. Ziv product bound on lz78PhraseStrings #

              theorem

              InformationTheory.Shannon.foldr_length_eq_map_sum

              source
              {α : Type u_1} [Fintype α] (ws : List (List α)) :
              List.foldr (fun (w : List α) (acc : ℕ) => w.length + acc) 0 ws = (List.map List.length ws).sum

              The foldr-length equals the map-length sum, bridging the total-length shape to the List.sum shape used by the packing lemma.

              Used by
                theorem

                InformationTheory.Shannon.lz78PhraseStrings_mul_log_le

                source
                {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (input : List α) :
                ↑(lz78PhraseStrings input).length * Real.log ↑(lz78PhraseStrings input).length ≤ 8 * Real.log (↑(Fintype.card α) + 1) * ↑input.length

                The Ziv product bound c·log c ≤ K·n on the greedy parse: the distinct phrase count c = (lz78PhraseStrings input).length satisfies c · log c ≤ 8·log(|α|+1) · input.length. This is the Cover–Thomas (★) for the longest-prefix greedy parse, combining the invariants lz78PhraseStrings_nodup / lz78PhraseStrings_forall_ne_nil / lz78PhraseStrings_total_length_le with the §3 packing core.

                Used by

                  §5. String → asymptotic-envelope bridge #

                  theorem

                  InformationTheory.Shannon.lz78PhraseStrings_mul_log_le_of_length

                  source
                  {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (input : ℕ → List α) (hlen : ∀ (n : ℕ), (input n).length = n) (n : ℕ) :
                  ↑(lz78PhraseStrings (input n)).length * Real.log ↑(lz78PhraseStrings (input n)).length ≤ 8 * Real.log (↑(Fintype.card α) + 1) * ↑n

                  The c·log c ≤ K·n bound for a length-n input family: for any family input : ℕ → List α with (input n).length = n, the distinct phrase count c(n) = (lz78PhraseStrings (input n)).length satisfies the Cover–Thomas product bound (★) with K = 8·log(|α|+1).

                  Used by
                    theorem

                    InformationTheory.Shannon.lz78PhraseStrings_count_isBigO

                    source
                    {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (input : ℕ → List α) (hlen : ∀ (n : ℕ), (input n).length = n) :
                    (fun (n : ℕ) => ↑(lz78PhraseStrings (input n)).length) =O[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n

                    The distinct phrase count of the longest-prefix greedy parse lz78PhraseStrings is O(n / log n): combining the product bound (★) (lz78PhraseStrings_mul_log_le) with the inversion lemma isBigO_natCast_div_log_of_mul_log_le (LZ78/PhraseCountAsymptotics.lean) gives c(n) = O(n / log n). This connects the distinct-phrase invariant to the Cover–Thomas envelope, with the length normalization (input n).length = n as the only hypothesis.

                    Used by