Skip to content

InformationTheory.Shannon.LZ78.ConverseUDObject

Imports 6

LZ78 converse UD-object #

This file builds the uniquely-decodable code object underlying LZ78 and applies Mathlib's McMillan inequality to it, obtaining a Kraft bound and an expectation-level source-coding converse for the LZ78 per-phrase (parent, symbol) token code.

What this delivers #

§1 — uniquelyDecodable_of_constantLength (general, reusable; Mathlib has no such constructor): any set of lists all of the same positive constant length K is UniquelyDecodable. This is the classic block-code fact and the mathematical core here — it is exactly the UD certificate the LZ78 token stream needs (lz78PhraseStrings itself is prefix-complete and not UD; the encoded fixed-width token set is).
§2 introduces boolEncode / finBoolCode, a concrete K-bit binary code m ↦ (range K).map (testBit m). Constant length K; injective on m < 2^K (Nat.eq_of_testBit_eq). finBoolCode encodes any Fintype whose card is ≤ 2^K as fixed-width binary, injectively.
§3 builds the LZ78 token code: for a dictionary of size c over alphabet α, the (c+1)·|α| possible (parent ∈ Fin (c+1), symbol ∈ α) tokens encode injectively into K = LZ78Phrase.bitLength c |α| bits ((c+1)·|α| ≤ 2^K via Nat.lt_pow_succ_log_self). Its image is UD (§1), so McMillan (McMillanKraftBridge) gives kraftSum 2 (fun _ => K) ≤ 1 and the Gibbs converse entropyD 2 P ≤ E[L] = K for the real LZ78 token code. K is exactly the per-phrase bit cost used in lz78GreedyEncodingLength = c · K (LZ78/AsymptoticOptimality/EncodingLength.lean).

Relation to the LZ78 block-rate converse #

The §3 converse is an expectation-level bound: it instantiates McMillanKraftBridge.entropyD_le_expectedLength_of_uniquelyDecodable at an explicitly constructed UD code rather than at an abstract UniquelyDecodable hypothesis. The LZ78 block-rate converse (Cover–Thomas, lz78Greedy_converse_ae in LZ78/AsymptoticOptimality/ParentBridgeConverse.lean) is instead an a.s.-eventual, per-realization liminf bound. Passing from the token-level Kraft bound to it needs the averaged ⟶ a.s. lift (Barron / competitive optimality), which runs through the polynomial block Kraft bound lz78_block_kraft_poly and Borel–Cantelli, not through this file.

§1. Constant-length codes are uniquely decodable #

theorem

InformationTheory.uniquelyDecodable_of_constantLength

{β : Type u_1} {S : Set (List β)} {K : ℕ} (hK : 0 < K) (hlen : ∀ w ∈ S, w.length = K) :

UniquelyDecodable S

A constant-length code is uniquely decodable (the block-code fact; Mathlib has no such constructor). If every codeword in S has the same positive length K, then distinct concatenations of codewords from S yield distinct strings.

Proof: equal flattens force equal codeword counts (length is K · count), and List.append_inj peels off equal-length heads one at a time.

Used by

§2. Fixed-width binary code #

def

InformationTheory.boolEncode

(K m : ℕ) :

The K-bit binary encoding of m: the booleans testBit m 0, …, testBit m (K-1). Constant length K.

Equations

InformationTheory.boolEncode K m = List.map m.testBit (List.range K)

Instances For

Used by

theorem

InformationTheory.boolEncode_length

@[simp]

(K m : ℕ) :

(boolEncode K m).length = K

Used by

theorem

InformationTheory.boolEncode_injOn

{K m m' : ℕ} (hm : m < 2 ^ K) (hm' : m' < 2 ^ K) (h : boolEncode K m = boolEncode K m') :

m = m'

boolEncode is injective on m < 2^K: agreeing on the low K bits plus both having no bits ≥ K (since m < 2^K) forces m = m'.

Used by

noncomputable def

InformationTheory.finBoolCode

(α' : Type u_2) [Fintype α'] (K : ℕ) (a : α') :

A fixed-width binary code for a Fintype: index each element via Fintype.equivFin, then K-bit encode. Constant length K.

Equations

InformationTheory.finBoolCode α' K a = InformationTheory.boolEncode K ↑((Fintype.equivFin α') a)

Instances For

Used by

theorem

InformationTheory.finBoolCode_length

@[simp]

{α' : Type u_1} [Fintype α'] (K : ℕ) (a : α') :

(finBoolCode α' K a).length = K

Used by

theorem

InformationTheory.injective_finBoolCode

{α' : Type u_1} [Fintype α'] {K : ℕ} (hcard : Fintype.card α' ≤ 2 ^ K) :

Function.Injective (finBoolCode α' K)

finBoolCode is injective when |α'| ≤ 2^K (so every index fits in K bits).

Used by

theorem

InformationTheory.uniquelyDecodable_finBoolCode

{α' : Type u_1} [Fintype α'] {K : ℕ} (hK : 0 < K) :

UniquelyDecodable ↑(Finset.image (finBoolCode α' K) Finset.univ)

The image of finBoolCode is uniquely decodable (constant length K > 0).

Used by

§3. The LZ78 `(parent, symbol)` token code #

theorem

InformationTheory.Shannon.lz78_token_card_le_pow

(c a : ℕ) :

(c + 1) * a ≤ 2 ^ LZ78Phrase.bitLength c a

The token count fits the per-phrase bit budget: a dictionary of size c has c+1 parent slots (incl. the empty-prefix root) times a symbols, and (c+1)·a ≤ 2^(bitLength c a) since bitLength c a = (log₂(c+1)+1)+(log₂ a+1) and n ≤ 2^(log₂ n + 1) (Nat.lt_pow_succ_log_self).

Used by

noncomputable def

InformationTheory.Shannon.lz78TokenCode

{α : Type u_1} [Fintype α] (c : ℕ) :

Fin (c + 1) × α → List Bool

The real LZ78 token code: a (parent, symbol) token for a dictionary of size c is encoded as a fixed-width K = bitLength c |α|-bit binary word. The parent ranges over Fin (c+1) (the c existing entries plus the empty-prefix root), the symbol over α.

Equations

InformationTheory.Shannon.lz78TokenCode c = InformationTheory.finBoolCode (Fin (c + 1) × α) (InformationTheory.Shannon.LZ78Phrase.bitLength c (Fintype.card α))

Instances For

Used by

theorem

InformationTheory.Shannon.lz78TokenCode_length

@[simp]

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (c : ℕ) (t : Fin (c + 1) × α) :

(lz78TokenCode c t).length = LZ78Phrase.bitLength c (Fintype.card α)

Every LZ78 token codeword has length K = bitLength c |α|.

Used by

theorem

InformationTheory.Shannon.lz78Token_card_le

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (c : ℕ) :

Fintype.card (Fin (c + 1) × α) ≤ 2 ^ LZ78Phrase.bitLength c (Fintype.card α)

The cardinality bound for the LZ78 token alphabet, |Fin (c+1) × α| ≤ 2^K.

Used by

theorem

InformationTheory.Shannon.injective_lz78TokenCode

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (c : ℕ) :

Function.Injective (lz78TokenCode c)

The LZ78 token code is injective.

Used by

theorem

InformationTheory.Shannon.uniquelyDecodable_lz78TokenCode

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (c : ℕ) :

UniquelyDecodable ↑(Finset.image (lz78TokenCode c) Finset.univ)

The LZ78 token codeword set is uniquely decodable (constant length K > 0).

Used by

theorem

InformationTheory.Shannon.lz78TokenCode_entropyD_le_expectedLength

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (c : ℕ) (P : MeasureTheory.Measure (Fin (c + 1) × α)) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (t : Fin (c + 1) × α), 0 < P.real {t}) :

ShannonCode.entropyD (↑(Fintype.card Bool)) P ≤ ShannonCode.expectedLength P fun (t : Fin (c + 1) × α) => (lz78TokenCode c t).length

The expectation-level source-coding converse for the LZ78 token code.

For any probability measure P (full support) on the LZ78 token alphabet, the binary entropy is bounded by the (constant) token code length:

entropyD 2 P ≤ E[L] = bitLength c |α|.

This is the Cover–Thomas converse, instantiated at the LZ78 (parent, symbol) token code via the McMillan bridge. The block-rate form (Cover–Thomas, lz78Greedy_converse_ae) needs the averaged ⟶ a.s. lift and is not addressed here.

Used by