InformationTheory.Shannon.LZ78.GreedyParsing

Imports 7

LZ78 greedy parsing — per-phrase bit length #

This file publishes the per-phrase bit-length cost of an LZ78 phrase: the number of bits needed to encode one (parent-index, symbol) pair given a dictionary size and an alphabet size. This is the Cover–Thomas per-phrase cost form

LZ78Phrase.bitLength c a = Nat.log 2 (c + 1) + Nat.log 2 a + 2

(each phrase index needs log(dictSize) bits, each appended symbol needs log(|α|) bits, plus a constant overhead). It is the shared infrastructure consumed by the genuine longest-prefix greedy encoding-length development (InformationTheory/Shannon/LZ78/AsymptoticOptimality.lean) and by the uniquely-decodable token code (InformationTheory/Shannon/LZ78/ConverseUDObject.lean).

File layout #

§1. Per-phrase bit length — LZ78Phrase.bitLength: the number of bits to encode one (parent-index, symbol) pair given a dictionary size and alphabet size, together with its simp normal form, monotonicity in the dictionary size, and positivity.

§1. Per-phrase bit length #

def

InformationTheory.Shannon.LZ78Phrase.bitLength

source

(c a : ℕ) :

ℕ

The bit length of a single LZ78 phrase.

Given dictionary size c and alphabet size a, encoding one phrase (parent, symbol) requires:

Nat.log 2 (c + 1) + 1 bits for the parent index (including the empty-prefix none, so the parent slot has c + 1 possibilities; + 1 for the floor-vs-ceil Nat.log gap).
Nat.log 2 a + 1 bits for the alphabet symbol.

This is the Cover–Thomas per-phrase cost form.

Equations