Skip to content

InformationTheory.Shannon.LZ78.Basic

Imports 7

Lempel–Ziv 78 asymptotic optimality #

Cover–Thomas (Universal Source Coding): for a stationary ergodic source {X_i} on a finite alphabet α, the per-symbol output length of the LZ78 dictionary code converges almost surely to the entropy rate:

lim_{n → ∞} (1/n) · ℓ(LZ78(X^n)) = H(𝓧)   a.s.

This is the universal source-coding analogue of Shannon's source-coding theorem: LZ78 achieves the entropy-rate lower bound without any prior knowledge of the source statistics.

File layout #

This single file publishes:

§1. LZ78 phrase data structures (LZ78Phrase α, LZ78Parsing α) — the type-level encoding of an LZ78 dictionary parsing.
§2. Generic sandwich combinator — lz78_asymptotic_optimality (and its alias / bundled forms), the LZ78-flavored wrapper of tendsto_of_le_liminf_of_limsup_le.

Scope of the §2 combinator #

lz78_asymptotic_optimality is not the LZ78 optimality theorem. It takes a generic encoding-length function lz78EncodingLength : ∀ n, (Fin n → α) → ℕ (the concrete greedy parse lz78Encode : List α → LZ78Parsing α is supplied externally), a generic limit L : ℝ, and a caller-supplied two-sided a.s. sandwich on the per-symbol rate — the liminf lower bound L ≤ liminf (lz/n), the limsup upper bound limsup (lz/n) ≤ L, and two boundedness arguments — and derives a.s. convergence of lz/n to L by tendsto_of_le_liminf_of_limsup_le (the same combine pattern as shannon_mcmillan_breiman_of_sandwich). Its h_lower / h_upper are hypotheses on whatever encoding the caller supplies, not a claim that some encoding achieves the entropy rate.

For the greedy LZ78 parser the two halves carry the substance: the achievability upper bound ∀ᵐ ω, limsup (lz/n) ≤ entropyRate₂ (Ziv's inequality, Cover–Thomas) and the converse lower bound ∀ᵐ ω, entropyRate₂ ≤ liminf (lz/n). They are lz78Greedy_achievability_ae (AsymptoticOptimality/ParentBridgeAchievability.lean) and lz78Greedy_converse_ae (AsymptoticOptimality/ParentBridgeConverse.lean); the headline instantiating the combinator with them at L = entropyRate₂ is lz78_asymptotic_optimality_with_greedy.

Re-use of existing infrastructure #

InformationTheory/Shannon/Stationary/Basic.lean (StationaryProcess / ErgodicProcess / blockRV), InformationTheory/Shannon/EntropyRate.lean (entropyRate, entropyRate_exists_of_stationary) and InformationTheory/Shannon/SMB/McMillanBreiman.lean (blockLogAvg, shannon_mcmillan_breiman_of_sandwich) are imported and used as black boxes; this file re-proves none of them.

§1. LZ78 phrase data structures #

structure

InformationTheory.Shannon.LZ78Phrase

(α : Type u_1) :

Type u_1

An LZ78 dictionary phrase is a pair (parent, symbol) where:

parent : Option ℕ references the earlier phrase being extended, or none for the empty-prefix root (the very first phrase ever emitted).
symbol : α is the single new alphabet symbol appended.

This is the Cover–Thomas dictionary entry encoded at the type level. Concrete lz78Encode : List α → LZ78Parsing α parsing is supplied externally; see the file-level docstring.

parent : Option ℕ
Reference to the parent phrase already in the dictionary; none marks the empty-prefix root.
symbol : α
The single alphabet symbol appended to the parent.

Instances For

Used by

def

InformationTheory.Shannon.LZ78Phrase.root

{α : Type u_1} (s : α) :

Root phrase: extend the empty prefix by a single symbol.

Equations

InformationTheory.Shannon.LZ78Phrase.root s = { parent := none, symbol := s }

Instances For

Used by

def

InformationTheory.Shannon.LZ78Phrase.cons

{α : Type u_1} (k : ℕ) (s : α) :

Extension phrase: extend the k-th dictionary entry by symbol s.

Equations

InformationTheory.Shannon.LZ78Phrase.cons k s = { parent := some k, symbol := s }

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.parent_root

@[simp]

{α : Type u_1} (s : α) :

(root s).parent = none

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.parent_cons

@[simp]

{α : Type u_1} (k : ℕ) (s : α) :

(cons k s).parent = some k

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.symbol_root

@[simp]

{α : Type u_1} (s : α) :

(root s).symbol = s

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.symbol_cons

@[simp]

{α : Type u_1} (k : ℕ) (s : α) :

(cons k s).symbol = s

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.ext_iff

{α : Type u_1} {p q : LZ78Phrase α} :

p = q ↔ p.parent = q.parent ∧ p.symbol = q.symbol

Two phrases are equal iff their parent and symbol agree.

Used by

structure

InformationTheory.Shannon.LZ78Parsing

(α : Type u_1) :

Type u_1

An LZ78 parsing of a finite input is a list of dictionary phrases together with the structural invariant that every parent = some k references an earlier (strictly smaller) phrase index.

This is the minimal Cover–Thomas LZ78 dictionary structure: a list of phrases whose parent references back-point into the already-emitted prefix of the list.

phrases : List (LZ78Phrase α)
The ordered list of dictionary phrases.
inRange(i : ℕ) (h : i < self.phrases.length) (k : ℕ) : (self.phrases.get ⟨i, h⟩).parent = some k → k < i
Structural invariant: every parent reference points to an earlier phrase index. The invariant is stated via List.get ⟨i, h⟩ (the total bounded-index accessor) so that the back-pointer constraint parent_i = some k → k < i is captured at the type level.

Instances For

Used by

def

InformationTheory.Shannon.LZ78Parsing.count

{α : Type u_1} (p : LZ78Parsing α) :

Number of phrases emitted by the parsing. Cover–Thomas notation: c(n).

Equations

p.count = p.phrases.length

Instances For

Used by

def

InformationTheory.Shannon.LZ78Parsing.empty

(α : Type u_2) :

The empty parsing, with no phrases.

Equations

InformationTheory.Shannon.LZ78Parsing.empty α = { phrases := [], inRange := ⋯ }

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.count_empty

@[simp]

(α : Type u_2) :

(empty α).count = 0

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.phrases_empty

@[simp]

(α : Type u_2) :

(empty α).phrases = []

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.count_eq_length

@[simp]

{α : Type u_1} (p : LZ78Parsing α) :

p.count = p.phrases.length

count is just the list length.

Used by

§2. Main theorem — LZ78 asymptotic optimality #

theorem

InformationTheory.Shannon.lz78_asymptotic_optimality

{α : Type u_1} {Ω : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) (lz78EncodingLength : (n : ℕ) → (Fin n → α) → ℕ) (L : ℝ) (h_lower : ∀ᵐ (ω : Ω) ∂μ, L ≤ Filter.liminf (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop) (h_upper : ∀ᵐ (ω : Ω) ∂μ, Filter.limsup (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop ≤ L) (h_bdd_above : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) (h_bdd_below : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop (nhds L)

The generic two-sided sandwich-combine lemma for per-symbol coding rates (the LZ78-flavored wrapper of tendsto_of_le_liminf_of_limsup_le).

This is not the LZ78 asymptotic-optimality claim itself. It is a generic combinator: given any encoding-length function lz78EncodingLength, any limit value L : ℝ, and a two-sided a.s. sandwich on the per-symbol rate (L ≤ liminf and limsup ≤ L, plus a.s. boundedness), it derives a.s. convergence of lz/n to L via tendsto_of_le_liminf_of_limsup_le (a 1-step squeeze). The hypotheses h_lower / h_upper are caller-supplied, not a claim that any particular encoding achieves any particular limit.

The limit L is left generic rather than hard-wired to entropyRate, so that the bit-rate headline lz78_asymptotic_optimality_with_greedy can instantiate it with the bit-unit entropyRate₂.

Used by

theorem

InformationTheory.Shannon.lz78_asymptotic_optimality_two_sided

{α : Type u_1} {Ω : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) (lz78EncodingLength : (n : ℕ) → (Fin n → α) → ℕ) (h_lower : ∀ᵐ (ω : Ω) ∂μ, entropyRate μ p.toStationaryProcess ≤ Filter.liminf (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop) (h_upper : ∀ᵐ (ω : Ω) ∂μ, Filter.limsup (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop ≤ entropyRate μ p.toStationaryProcess) (h_bdd_above : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) (h_bdd_below : ∀ᵐ (ω : Ω) ∂μ, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop (nhds (entropyRate μ p.toStationaryProcess))

The generic two-sided sandwich-combine, alias form.

Alias for the generic combinator lz78_asymptotic_optimality with the same four arguments (liminf lower bound, limsup upper bound, two Filter.IsBoundedUnder boundedness arguments), specialized to L = entropyRate μ p. Like its target this is not the LZ78 optimality claim — h_lower / h_upper are caller-supplied sandwich arguments.

Used by

theorem

InformationTheory.Shannon.lz78_asymptotic_optimality_of_bounds

{α : Type u_1} {Ω : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ErgodicProcess μ α) (lz78EncodingLength : (n : ℕ) → (Fin n → α) → ℕ) (h_combined : ∀ᵐ (ω : Ω) ∂μ, entropyRate μ p.toStationaryProcess ≤ Filter.liminf (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop ∧ Filter.limsup (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop ≤ entropyRate μ p.toStationaryProcess ∧ (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ↑(lz78EncodingLength n (p.blockRV n ω)) / ↑n) Filter.atTop (nhds (entropyRate μ p.toStationaryProcess))

The generic two-sided sandwich-combine, bundled-conjunction form.

Bundles the four sandwich arguments into a single conjunction h_combined (lower / upper / above / below); the body destructures and forwards to lz78_asymptotic_optimality_two_sided. As with its target this is not the LZ78 optimality claim — the bundled lower / upper conjuncts are caller-supplied sandwich arguments.

Used by