Skip to content

InformationTheory.Shannon.LZ78.ConverseAsymptotic

Imports 7

LZ78 converse — asymptotic body extension #

This file publishes the asymptotic-body layer on top of the combinatorial ZivCountingBound predicate already published in InformationTheory/Shannon/LZ78/ZivInequality.lean. It is a predicate-level extension: the per-n real-valued bound (p.count : ℝ) ≤ B is lifted to families (p : ℕ → LZ78Parsing α) indexed by the block length, and the asymptotic shape c(n) · log c(n) ≤ n · log b + O(1) (Cover–Thomas, the Ziv-counting asymptotic) is exposed as a hypothesis pass-through IsLZ78PhraseCountAsymptotic that future discharges can plug in. The genuine a.s. achievability residual is scoped out as lz78Greedy_achievability_ae in AsymptoticOptimality.lean.

Scope #

(engaged) — IsLZ78PhraseCountAsymptotic predicate shaped on Asymptotics.IsBigO atTop, plus a .trivial constructor.
(engaged) — IsZivCountingAsymptoticBound per-n bound aggregator with .refl, .mono, .add_nonneg, and .of_pointwise_count constructors.
(engaged) — bridge theorems showing how a uniform per-n Ziv counting bound implies the asymptotic predicate.
(deferred) — the concrete derivation of c(n) ≤ n / log_b n · (1 + o(1)) from Cover–Thomas is supplied as hypothesis; the numerical asymptotic c(n) · log c(n) − n · log b = o(n) is the Cover–Thomas body and remains out of scope here.

Pattern source #

Follows the same "predicate + .trivial + bridge" pattern as ZivInequality.lean. The asymptotic layer is wrapped in Asymptotics.IsBigO notation so downstream callers can plug Mathlib.Analysis.Asymptotics lemmas directly without re-shaping.

§1. `IsZivCountingAsymptoticBound` per-`n` predicate #

def

InformationTheory.Shannon.IsZivCountingAsymptoticBound

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

The per-n Ziv counting asymptotic-bound predicate.

For a family of parsings p : ℕ → LZ78Parsing α indexed by block length, this predicate asserts a uniform per-n real-valued upper bound on ((p n).count : ℝ) by B n. The bound function B : ℕ → ℝ plays the role of the Cover–Thomas asymptotic envelope n / log_b n · (1 + o(1)); concrete witnesses come from card_phraseSet_le_pow-style combinatorial counts.

Equations

InformationTheory.Shannon.IsZivCountingAsymptoticBound p B = ∀ (n : ℕ), ↑(p n).count ≤ B n

Instances For

Used by

theorem

InformationTheory.Shannon.IsZivCountingAsymptoticBound.refl

@[simp]

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

IsZivCountingAsymptoticBound p fun (n : ℕ) => ↑(p n).count

Used by

theorem

InformationTheory.Shannon.IsZivCountingAsymptoticBound.mono

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B B' : ℕ → ℝ} (h : IsZivCountingAsymptoticBound p B) (hB : ∀ (n : ℕ), B n ≤ B' n) :

IsZivCountingAsymptoticBound p B'

Monotonicity in the bound function.

Used by

theorem

InformationTheory.Shannon.IsZivCountingAsymptoticBound.add_nonneg

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B ε : ℕ → ℝ} (h : IsZivCountingAsymptoticBound p B) (hε : ∀ (n : ℕ), 0 ≤ ε n) :

IsZivCountingAsymptoticBound p fun (n : ℕ) => B n + ε n

If B bounds count, so does B + ε for any non-negative slack ε.

Used by

theorem

InformationTheory.Shannon.IsZivCountingAsymptoticBound.of_pointwise_count

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B : ℕ → ℝ} (h : ∀ (n : ℕ), ZivCountingBound (p n) (B n)) :

IsZivCountingAsymptoticBound p B

Lift a pointwise ZivCountingBound to the asymptotic family: if for every n the per-n parsing p n satisfies ZivCountingBound (p n) (B n), then the asymptotic predicate holds.

Used by

§2. `IsLZ78PhraseCountAsymptotic` predicate #

def

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic

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

The asymptotic phrase-count predicate.

For a family of LZ78 parsings p : ℕ → LZ78Parsing α and a reference envelope function B : ℕ → ℝ (in the textbook this is n ↦ n / Real.log n or similar), this predicate asserts that the phrase-count sequence n ↦ ((p n).count : ℝ) is O[atTop] of B.

Cover–Thomas reads c(n) ≤ n / log_b(c(n)) ≤ n / log_b n · (1 + o(1)), and this predicate captures exactly the IsBigO half: the (1 + o(1)) slack is absorbed into the constant of IsBigO.

Equations

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic p B = (fun (n : ℕ) => ↑(p n).count) =O[Filter.atTop ] B

Instances For

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.refl

@[simp]

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

IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑(p n).count

A sequence is trivially O[atTop] of itself.

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.of_eventual_le

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B : ℕ → ℝ} (h_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop , 0 ≤ B n) (h_le : ∀ᶠ (n : ℕ) in Filter.atTop , ↑(p n).count ≤ B n) :

IsLZ78PhraseCountAsymptotic p B

Trivial constructor from a global numeric upper bound (in particular: a uniform (p n).count ≤ B n with B n ≥ 0).

Used by

§3. Pure asymptotic algebra layer #

§5. Trivial-`n`-envelope bridges #

theorem

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.linear_of_count_le_n

{α : Type u_1} {p : ℕ → LZ78Parsing α} (h_le : ∀ (n : ℕ), (p n).count ≤ n) :

IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n

The linear envelope from a uniform count ≤ n bound. Under the trivial parsing-invariant constraint (p n).count ≤ n (which holds for any LZ78 parsing of a length-n input), the phrase-count sequence is O[atTop] (fun n => (n : ℝ)).

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.of_ZivCountingBound

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B : ℕ → ℝ} (h_bound : ∀ (n : ℕ), ZivCountingBound (p n) (B n)) (h_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop , 0 ≤ B n) :

IsLZ78PhraseCountAsymptotic p B

If for every n the per-n Ziv counting bound holds with a real envelope B n, and B is eventually non-negative, then the asymptotic predicate holds. This is the ergonomic entry point when the upstream caller already has the per-n ZivCountingBound lemma.

Used by

§6. `Real.log`-style envelopes #

theorem

InformationTheory.Shannon.natCast_div_real_log_eventually_nonneg

:

∀ᶠ (n : ℕ) in Filter.atTop , 0 ≤ ↑n / Real.log ↑n

The n / Real.log n envelope is eventually non-negative. Cover–Thomas envelope sanity.

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.of_n_div_log

{α : Type u_1} {p : ℕ → LZ78Parsing α} (h_bound : ∀ᶠ (n : ℕ) in Filter.atTop , ↑(p n).count ≤ ↑n / Real.log ↑n) :

IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n / Real.log ↑n

The asymptotic phrase-count predicate from a n / Real.log n bound. The textbook-form constructor: given a per-n bound (p n).count ≤ n / Real.log n + slack, with the slack itself bounded above by n / Real.log n asymptotically, conclude IsLZ78PhraseCountAsymptotic p (fun n => (n : ℝ) / Real.log n).

Used by

§7. Main result — phrase-count asymptotic upper bound #

theorem

InformationTheory.Shannon.lz78_phrase_count_asymptotic

{α : Type u_1} (p : ℕ → LZ78Parsing α) (B : ℕ → ℝ) (h_bound : ∀ (n : ℕ), ZivCountingBound (p n) (B n)) (h_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop , 0 ≤ B n) :

IsLZ78PhraseCountAsymptotic p B

LZ78 phrase-count asymptotic upper bound, in hypothesis pass-through form. For any family of LZ78 parsings p : ℕ → LZ78Parsing α and any real-valued envelope B : ℕ → ℝ, if the per-n Ziv counting bound (p n).count ≤ B n holds and B is eventually non-negative, then the asymptotic predicate IsLZ78PhraseCountAsymptotic p B holds.

This is the predicate-level statement of Cover–Thomas, shaped so that downstream callers can supply any concrete envelope function (e.g. n / log_b n, n / log n, n) without changing the external signature. The substantive arithmetic c(n) · log c(n) ≤ n · log b + O(1) (Cover–Thomas asymptotic body) remains out of scope here, but is encapsulated inside B n and so does not surface in this signature.

Pattern: the same hypothesis pass-through style as relay_cutset_outer_bound.

Used by

theorem

InformationTheory.Shannon.lz78_phrase_count_asymptotic_n_div_log

{α : Type u_1} (p : ℕ → LZ78Parsing α) (h_bound : ∀ᶠ (n : ℕ) in Filter.atTop , ↑(p n).count ≤ ↑n / Real.log ↑n) :

IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n / Real.log ↑n

Specialized to the n / Real.log n envelope (Cover–Thomas).

Used by

theorem

InformationTheory.Shannon.lz78_phrase_count_asymptotic_linear

{α : Type u_1} (p : ℕ → LZ78Parsing α) (h_le : ∀ (n : ℕ), (p n).count ≤ n) :

IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n

Specialized to the linear n envelope (the trivial bound).

Used by

§8. Two-sided / sandwich-form combine #

def

InformationTheory.Shannon.IsLZ78PhraseCountSandwich

{α : Type u_1} (p : ℕ → LZ78Parsing α) (B_lower B_upper : ℕ → ℝ) :

Combine an upper-bound predicate IsLZ78PhraseCountAsymptotic p B_upper and a lower-bound predicate B_lower =O[atTop] (p.count) (i.e. the phrase count dominates B_lower) into a sandwich. This is the predicate-level analogue of the Cover–Thomas ⟺ sandwich.

Equations

InformationTheory.Shannon.IsLZ78PhraseCountSandwich p B_lower B_upper = (InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic p B_upper ∧ B_lower =O[Filter.atTop ] fun (n : ℕ) => ↑(p n).count)

Instances For

Used by

theorem

InformationTheory.Shannon.isLZ78PhraseCountSandwich_def

@[simp]

{α : Type u_1} (p : ℕ → LZ78Parsing α) (B_lower B_upper : ℕ → ℝ) :

IsLZ78PhraseCountSandwich p B_lower B_upper ↔ IsLZ78PhraseCountAsymptotic p B_upper ∧ B_lower =O[Filter.atTop ] fun (n : ℕ) => ↑(p n).count

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountSandwich.refl

@[simp]

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

IsLZ78PhraseCountSandwich p (fun (n : ℕ) => ↑(p n).count) fun (n : ℕ) => ↑(p n).count

Any parsing family sandwiches its own count.

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountSandwich.upper

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B_lower B_upper : ℕ → ℝ} (h : IsLZ78PhraseCountSandwich p B_lower B_upper) :

IsLZ78PhraseCountAsymptotic p B_upper

Sandwich destructor: upper bound.

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountSandwich.lower

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B_lower B_upper : ℕ → ℝ} (h : IsLZ78PhraseCountSandwich p B_lower B_upper) :

B_lower =O[Filter.atTop ] fun (n : ℕ) => ↑(p n).count

Sandwich destructor: lower bound.

Used by

theorem

InformationTheory.Shannon.IsLZ78PhraseCountSandwich.mk

{α : Type u_1} {p : ℕ → LZ78Parsing α} {B_lower B_upper : ℕ → ℝ} (h_upper : IsLZ78PhraseCountAsymptotic p B_upper) (h_lower : B_lower =O[Filter.atTop ] fun (n : ℕ) => ↑(p n).count) :

IsLZ78PhraseCountSandwich p B_lower B_upper

Sandwich constructor from two asymptotic ingredients.

Used by

§9. Bridge to the LZ78SMBSandwich entrypoints #