InformationTheory.Shannon.LZ78.ZivEntropyBridge

Imports 6

LZ78 Ziv-inequality entropy bridge — foundational lemmas #

This file hosts the foundational, mutually-independent lemmas of the LZ78 Ziv-inequality entropy bridge (Cover–Thomas), built on top of the SMB layer (blockLogAvg, SMB/McMillanBreiman.lean).

Main statements #

log_sum_inequality — the (finite) log-sum inequality (∑ aᵢ)·log((∑aᵢ)/(∑bᵢ)) ≤ ∑ aᵢ·log(aᵢ/bᵢ), derived from convexity of x ↦ x·log x (Real.convexOn_mul_log) via finite Jensen (ConvexOn.map_sum_le).
blockLogAvg_eq_neg_log_blockProb — the trivial restatement n · blockLogAvg μ p n ω = -log Pₙ{block ω} for 0 < n, the form the Ziv chain consumes.

Per-path parsing factorization #

The Ziv chain (Cover–Thomas) needs the pushforward block probability Pₙ{block ω} bounded above by a product of per-phrase conditional probabilities along the LZ78 parse: Pₙ ≤ ∏ⱼ qⱼ. This inequality is unconditionally true by prefix monotonicity (blockProb_le_prod_condPhraseProb, Stationary/Kernel.lean); the equality Pₙ = ∏ⱼ qⱼ is false for the longest-prefix parse (it leaves an unfinished tail, so boundary c ≤ n and the product equals prefixBlockProb ω (boundary c) ≥ Pₙ).

condPhraseProb — the per-phrase conditional probability indexed by phrase position j, defined concretely as the ratio of successive parsing-prefix block probabilities (telescoping to prefixBlockProb ω (boundary c)).
IsLZ78PerPathParsingFactorization — the named Prop carrying the Ziv inequality Pₙ{block ω} ≤ ∏ⱼ condPhraseProb … plus a positivity field; constructible from positivity alone (isLZ78PerPathParsingFactorization_of_pos, Stationary/Kernel.lean).
blockProb_neg_log_ge_sum — from that factorization, ∑ⱼ -log (condPhraseProb …) ≤ -log Pₙ{block ω} (the direction the Ziv chain consumes), given 0 < Pₙ (a.s. regularity).

The combinatorial c·log c ≤ -log Pₙ core of the per-path Ziv inequality is ziv_achievability_composition (ZivAchievabilityComposition.lean), and the achievability / converse assembly is in AsymptoticOptimality/; this file supplies the base they rest on.

theorem

InformationTheory.Shannon.log_sum_inequality

source

{ι : Type u_3} (s : Finset ι) (a b : ι → ℝ) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 < b i) :

(∑ i ∈ s, a i) * Real.log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i) ≤ ∑ i ∈ s, a i * Real.log (a i / b i)

The log-sum inequality (finite form).

For nonnegative aᵢ and strictly positive bᵢ over a finite index set s, (∑ aᵢ)·log((∑ aᵢ)/(∑ bᵢ)) ≤ ∑ aᵢ·log(aᵢ/bᵢ).

Proved from convexity of x ↦ x·log x (Real.convexOn_mul_log) via finite Jensen (ConvexOn.map_sum_le) with weights bᵢ/(∑ b) and points aᵢ/bᵢ.

Used by

theorem

InformationTheory.Shannon.blockLogAvg_eq_neg_log_blockProb

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) {n : ℕ} (hn : 0 < n) (ω : Ω) :

↑n * blockLogAvg μ p n ω = -Real.log ((MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω})

Restatement of blockLogAvg as a negative log block-probability.

For 0 < n, n · blockLogAvg μ p n ω = -log Pₙ{block ω} where Pₙ = μ.map (blockRV n). Trivial unfolding of the blockLogAvg definition; this is the form the per-path Ziv inequality consumes.

Used by

Per-path parsing factorization #

def

InformationTheory.Shannon.parsingBoundary

source

{α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (j : ℕ) :

ℕ

The cumulative parsing boundary length.

The number of input symbols consumed by the first j emitted LZ78 phrases of the observed block blockRV n ω, i.e. the sum of the lengths of the first j distinct phrase strings. Used as a blockRV index to read the block probability of the corresponding parsing prefix.

Equations

InformationTheory.Shannon.parsingBoundary μ p n ω j = (List.map List.length (List.take j (InformationTheory.Shannon.lz78PhraseStrings (List.ofFn (p.blockRV n ω))))).sum

Instances For

Used by

noncomputable def

InformationTheory.Shannon.prefixBlockProb

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (ω : Ω) (m : ℕ) :

ℝ

The prefix block probability.

The pushforward block probability of the length-m parsing prefix of the observed path, Pₘ{blockRV m ω} = (μ.map (blockRV m)).real {blockRV m ω}.

Equations

InformationTheory.Shannon.prefixBlockProb μ p ω m = (MeasureTheory.Measure.map (p.blockRV m) μ).real {p.blockRV m ω}

Instances For

Used by

noncomputable def

InformationTheory.Shannon.condPhraseProb

source

{α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (j : ℕ) :

ℝ

The per-phrase conditional probability (Cover–Thomas, chain-rule per-path form), indexed by phrase position j.

Concretely the ratio of the block probabilities of the parsing prefix after j+1 phrases and after j phrases: condPhraseProb μ p n ω j = Pₘ₊₁{prefix} / Pₘ{prefix} where m-prefix is the prefix ending at the j-th phrase boundary. Over the phrase positions of the parse this product telescopes to Pₙ{block ω} — the content of IsLZ78PerPathParsingFactorization.

This is ℝ-valued so that Real.log_prod applies directly in blockProb_neg_log_ge_sum (Mathlib-shape-driven: the dominant downstream lemma is Real.log_prod).

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

structure

InformationTheory.Shannon.IsLZ78PerPathParsingFactorization

source

{α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) :

Prop

The per-path block probability of a stationary process is bounded above by the product of the LZ78 parse's per-phrase conditional probabilities, Pₙ{block ω} ≤ ∏ⱼ condPhraseProb … (Cover–Thomas, the per-path / per-realization form of the entropy chain rule, in the inequality direction the Ziv chain consumes).

The factorization is stated as an inequality rather than the equality Pₙ = ∏ⱼ qⱼ, which is false in general: the longest-prefix greedy parse leaves an unfinished tail, so the phrase boundaries cover only boundary c ≤ n symbols and the telescoping product equals prefixBlockProb ω (boundary c) ≥ Pₙ; requiring the equality would make IsLZ78PerPathParsingFactorization unsatisfiable for non-completing parses. The inequality is all the Ziv chain needs and holds unconditionally by prefix monotonicity of the cylinder block probability (blockProb_le_prod_condPhraseProb / isLZ78PerPathParsingFactorization_of_pos, Stationary/Kernel.lean), constructed from positivity alone (a.s. regularity), not assumed.

The pos field records strict positivity of each conditional factor over the phrase positions; this is a.s. regularity (each observed cylinder has positive mass) and discharges the side condition of Real.log_prod in blockProb_neg_log_ge_sum.

factor(n : ℕ) (ω : Ω) : (MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω} ≤ ∏ j ∈ Finset.range (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length, condPhraseProb μ p n ω j
The block probability is bounded above by the product of per-phrase conditional probabilities over the parse (the Ziv direction).
pos(n : ℕ) (ω : Ω) (j : ℕ) : j ∈ Finset.range (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length → 0 < condPhraseProb μ p n ω j
Each conditional factor is strictly positive over the phrase positions of the parse (positivity side condition for Real.log_prod).

Instances For

Used by

theorem

InformationTheory.Shannon.blockProb_neg_log_ge_sum

source

{α : Type u_1} {Ω : Type u_2} [DecidableEq α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (h : IsLZ78PerPathParsingFactorization μ p) (n : ℕ) (ω : Ω) (hPn : 0 < (MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω}) :

∑ j ∈ Finset.range (lz78PhraseStrings (List.ofFn (p.blockRV n ω))).length, -Real.log (condPhraseProb μ p n ω j) ≤ -Real.log ((MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω})

The factorization in additive log form.

From the Ziv-direction factorization, the sum, over the phrase positions of the parse, of the negative logs of the per-phrase conditional probabilities is bounded above by the negative log block probability: ∑ⱼ -log (condPhraseProb …) ≤ -log Pₙ{block ω}.

This is the inequality direction the per-path Ziv chain consumes: the factorization is Pₙ ≤ ∏ⱼ qⱼ, so -log reverses it to ≥. Proved via Real.log_prod (positivity of each factor supplied by the pos field) and monotonicity of Real.log (positivity of Pₙ is the a.s. regularity hypothesis hPn — the observed block has positive mass). Combined with blockLogAvg_eq_neg_log_blockProb it bounds the per-phrase sum by n · blockLogAvg.

Used by

Base-2 (bit) layer — unit correction for the LZ78 headline #

The LZ78 encoding length lz78GreedyEncodingLength (LZ78/AsymptoticOptimality/EncodingLength.lean) is measured in bits (LZ78Phrase.bitLength uses Nat.log 2, the binary code-length), whereas blockLogAvg / entropyRate are natural-log quantities (nats). The Cover–Thomas statement is bit-based:

(lz n x)/n → H₂   where  H₂ = (entropy rate in bits) = entropyRate / log 2.

We therefore introduce the base-2 (bit) versions blockLogAvg₂ and entropyRate₂ as the natural-log quantities divided by Real.log 2. These are unit conversions, not new content: blockLogAvg₂ = blockLogAvg / log 2 converges to entropyRate₂ = entropyRate / log 2 directly from SMB. The LZ78 achievability / converse bounds, being bit-based (c·log₂c ≤ -log₂ Pₙ), are stated against blockLogAvg₂.

theorem

InformationTheory.Shannon.log_two_pos

source

0 < Real.log 2

0 < Real.log 2 — the unit-conversion constant between nats and bits.

Used by