Skip to content

InformationTheory.Shannon.LZ78.ZivInequality

Imports 8

LZ78 Ziv's inequality — combinatorial counting layer #

This file publishes the combinatorial counting plumbing layer of Ziv's inequality (Cover–Thomas; the upper-bound half of the LZ78 asymptotic optimality theorem). It establishes the combinatorial layer (Nat-level phrase-space cardinality bound) as concrete theorems, consumed by the IsLZ78PhraseCountAsymptotic asymptotic layer; the entropy layer (H(X^n) ≤ Σ H(phrase_i)) and the log-sum layer (final Ziv form) are developed elsewhere. The genuine a.s. achievability residual of LZ78 optimality is scoped out as lz78Greedy_achievability_ae in AsymptoticOptimality.lean.

File layout #

§1. LZ78Phrase cardinality plumbing — LZ78Phrase.equivOptionNatProd-style cardinality / image-card bounds.
§2. LZ78Parsing.count combinatorial bounds — Nat-level inequalities on p.count = p.phrases.length purely from the parsing invariant.
§3. ZivCountingBound predicate — a real-valued predicate that exposes the combinatorial-layer Ziv counting bound at the Prop level, with a .refl constructor and a constructor taking a real bound directly. The entropy-side layer plugs ZivCountingBound into the IsLZ78PhraseCountAsymptotic envelope.

Scope #

Combinatorial counting bound: LZ78Parsing.count_le_card_phrase_space and friends. Pure Nat/Finset, no measure-theoretic infrastructure.
ZivCountingBound real-valued Prop slot.
Entropy chain-rule layer (H(X^n) ≤ Σ H(phrase_i)), developed elsewhere.
Log-sum + final Ziv inequality main form, developed elsewhere.

Pattern source #

The "extract the most tractable fragments" pattern is the same as InformationTheory/Shannon/WynerZiv/RateMonotonicity.lean: the parent placeholder is not fully discharged; the file publishes the fragments that are tractable now plus a real-valued predicate exposing the layered shape, with .trivial bridges to the parent placeholder.

§1. `LZ78Phrase` cardinality plumbing #

def

InformationTheory.Shannon.LZ78Phrase.parentBounded

(c : ℕ) (α : Type u_2) :

Type u_2

An LZ78 phrase whose parent is in Option (Fin c) (i.e. either the empty-prefix root none, or a back-reference some k with k < c). This is the natural ambient finite type that bounds the dictionary phrase space after the first c phrases have been emitted: each subsequent phrase is (parent ∈ {none, some 0, ..., some (c-1)}) × (symbol ∈ α).

Equations

InformationTheory.Shannon.LZ78Phrase.parentBounded c α = (Option (Fin c) × α)

Instances For

Used by

instance

InformationTheory.Shannon.LZ78Phrase.parentBounded_fintype

@[implicit_reducible]

(c : ℕ) (α : Type u_2) [Fintype α] :

Fintype (parentBounded c α)

Equations

InformationTheory.Shannon.LZ78Phrase.parentBounded_fintype c α = id inferInstance

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.card_parentBounded

@[simp]

(c : ℕ) (α : Type u_2) [Fintype α] :

Fintype.card (parentBounded c α) = (c + 1) * Fintype.card α

Cardinality of the bounded-parent phrase space: (c + 1) · |α|.

Used by

def

InformationTheory.Shannon.LZ78Phrase.ofParentBounded

{c : ℕ} (α : Type u_2) (pb : parentBounded c α) :

The "embed-with-bound" function from parentBounded c α back into LZ78Phrase α: forget the bound.

Equations

InformationTheory.Shannon.LZ78Phrase.ofParentBounded α pb = { parent := Option.map (fun (x : Fin c) => ↑x) pb.1, symbol := pb.2 }

Instances For

Used by

def

InformationTheory.Shannon.LZ78Phrase.boundParent

{c : ℕ} (o : Option ℕ) :

(∀ (k : ℕ), o = some k → k < c) → Option (Fin c)

Convert an Option ℕ whose some k case satisfies k < c into Option (Fin c). The "round-trip" forget-then-attach direction.

Equations

InformationTheory.Shannon.LZ78Phrase.boundParent none x_2 = none
InformationTheory.Shannon.LZ78Phrase.boundParent (some k) h = some ⟨k, ⋯⟩

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.boundParent_none

@[simp]

{c : ℕ} (h : ∀ (k : ℕ), none = some k → k < c) :

boundParent none h = none

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.boundParent_some

@[simp]

{c : ℕ} (k : ℕ) (h : ∀ (k' : ℕ), some k = some k' → k' < c) :

boundParent (some k) h = some ⟨k, ⋯⟩

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.map_val_boundParent

@[simp]

{c : ℕ} (o : Option ℕ) (h : ∀ (k : ℕ), o = some k → k < c) :

Option.map (fun (x : Fin c) => ↑x) (boundParent o h) = o

Used by

def

InformationTheory.Shannon.LZ78Phrase.toParentBounded

{α : Type u_1} {c : ℕ} (ph : LZ78Phrase α) (h : ∀ (k : ℕ), ph.parent = some k → k < c) :

parentBounded c α

Convert an LZ78Phrase whose parent is either none or some k with k < c into the bounded type parentBounded c α.

Equations

ph.toParentBounded h = (InformationTheory.Shannon.LZ78Phrase.boundParent ph.parent h, ph.symbol)

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Phrase.ofParentBounded_toParentBounded

@[simp]

{α : Type u_1} {c : ℕ} (ph : LZ78Phrase α) (h : ∀ (k : ℕ), ph.parent = some k → k < c) :

ofParentBounded α (ph.toParentBounded h) = ph

Used by

§2. `LZ78Parsing.count` combinatorial bounds #

theorem

InformationTheory.Shannon.LZ78Parsing.count_eq_length'

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

p.count = p.phrases.length

LZ78Parsing.count is the list length. Restatement of LZ78Parsing.count_eq_length for direct citation in counting proofs.

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.count_empty'

@[simp]

{α : Type u_1} :

(empty α).count = 0

The empty parsing has count zero.

Used by

noncomputable def

InformationTheory.Shannon.LZ78Parsing.phraseSet

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

Finset (LZ78Phrase α)

The set of phrases of a parsing, as a finset. Built by mapping the Fin p.count index space through the get accessor and packaging as a Finset via Finset.image. Uses Classical.decEq so that no DecidableEq instance on LZ78Phrase α is required at the call site.

Equations

p.phraseSet = Finset.image (fun (i : Fin p.phrases.length) => p.phrases.get i) Finset.univ

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.parent_bounded

{α : Type u_1} (p : LZ78Parsing α) (i : ℕ) (hi : i < p.phrases.length) (k : ℕ) :

(p.phrases.get ⟨i, hi⟩).parent = some k → k < p.phrases.length

Every phrase in the parsing has bounded parent. Direct consequence of the inRange invariant: phrase at index i < count has parent in Option (Fin count).

Used by

noncomputable def

InformationTheory.Shannon.LZ78Parsing.indexToBounded

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

Fin p.phrases.length → LZ78Phrase.parentBounded p.phrases.length α

The phrase-index map factors through parentBounded. Map each Fin p.count index to its corresponding bounded-parent phrase, then forget the bound to recover the phrase itself.

Equations

p.indexToBounded i = (p.phrases.get i).toParentBounded ⋯

Instances For

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.ofParentBounded_indexToBounded

{α : Type u_1} (p : LZ78Parsing α) (i : Fin p.phrases.length) :

LZ78Phrase.ofParentBounded α (p.indexToBounded i) = p.phrases.get i

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.card_phraseSet_le_pow

{α : Type u_1} [Fintype α] (p : LZ78Parsing α) :

p.phraseSet.card ≤ (p.count + 1) * Fintype.card α

The count upper bound via the bounded-parent ambient. For any LZ78 parsing on a finite alphabet, the number of distinct phrases is at most (count + 1) · |α|: every phrase is a pair (parent ∈ Option (Fin count), symbol ∈ α).

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.count_nonneg

@[simp]

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

Trivial monotonicity: count ≥ 0. A useful base hypothesis for Ziv-style real-valued bounds (avoids pos/nonneg re-derivation downstream).

Used by

theorem

InformationTheory.Shannon.LZ78Parsing.phraseSet_empty

@[simp]

{α : Type u_1} :

(empty α).phraseSet = ∅

The empty parsing has an empty phrase set.

Used by

§3. `ZivCountingBound` predicate #

def

InformationTheory.Shannon.ZivCountingBound

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

The real-valued Ziv counting-layer predicate.

For a parsing p and a real-valued upper bound B : ℝ, this predicate asserts that the combinatorial layer of the Ziv inequality holds: the cast (p.count : ℝ) is bounded by B. The predicate is shaped so that the entropy-side layer can supply B = n / log c(n) (Cover–Thomas) or any analogous real-valued upper bound and plug it into the IsLZ78PhraseCountAsymptotic envelope.

The combinatorial layer of B is established by card_phraseSet_le_pow (§2); the entropy / log-sum layers are developed elsewhere.

Equations

InformationTheory.Shannon.ZivCountingBound p B = (↑p.count ≤ B)

Instances For

Used by

theorem

InformationTheory.Shannon.ZivCountingBound.refl

@[simp]

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

ZivCountingBound p ↑p.count

Trivially count ≤ count.

Used by

theorem

InformationTheory.Shannon.ZivCountingBound.mono

{α : Type u_1} {p : LZ78Parsing α} {B B' : ℝ} (h : ZivCountingBound p B) (hB : B ≤ B') :

ZivCountingBound p B'

Monotonicity in the real bound.

Used by

theorem

InformationTheory.Shannon.ZivCountingBound.add_nonneg

{α : Type u_1} {p : LZ78Parsing α} {B ε : ℝ} (h : ZivCountingBound p B) (hε : 0 ≤ ε) :

ZivCountingBound p (B + ε)

Adding a positive slack preserves the bound (B ≤ B + ε).

Used by