InformationTheory

InformationTheory.Shannon.LZ78.EmpiricalEntropyMean

source

Imports 8

LZ78 overhead control — empirical-entropy / mean bound #

This file supplies the analytic crux behind the o(n) overhead estimate required by the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (InformationTheory/Shannon/LZ78/AsymptoticOptimality.lean).

Approach #

The generic length-grouping inequality (card_mul_log_le_sum_group_mul_log_add_card_log) controls c · log c ≤ ∑ … + c · log D with a worst-case overhead c · log D, where D is the number of distinct lengths. For the LZ78 parse D ~ √n, so c · log D ~ Θ(n) does not vanish. The correct, sharper overhead is the empirical entropy of the length profile, ∑_g c_g · log (c / c_g), and the key analytic fact is that this empirical entropy is controlled by the (log of the) mean length under the average-length constraint ∑_l l · c_l = N.

The proof is a one-shot application of the log-sum inequality (a pure Finset/Real statement, derived here from convexity of x ↦ x · log x) with a geometric reference distribution b_l = θ^{l-1} whose parameter θ = 1 - C/N matches the empirical mean N/C. Concretely:

∑_l c_l · log (C / c_l) ≤ C · log (N / C) + C.

The constant κ = 1 is forced by the geometric reference (a log 2 slack survives the uniform-profile check), and C · log (N/C) = C · log(mean) is the o(n) term once mean ~ log n is supplied downstream.

Main result #

theorem

InformationTheory.Shannon.logSumInequality

source
{ι : Type u_1} (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, local copy).

For nonnegative a and strictly positive b over a finite index set s, (∑ a)·log((∑ a)/(∑ b)) ≤ ∑ aᵢ·log(aᵢ/bᵢ). Convexity of x ↦ x·log x through finite Jensen. (Re-proved locally to keep this file measure-free.)

Used by
    theorem

    InformationTheory.Shannon.sum_geom_shift_le_inv

    source
    (L : Finset ℕ) (θ : ℝ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hl1 : ∀ l ∈ L, 1 ≤ l) :
    ∑ l ∈ L, θ ^ (l - 1) ≤ (1 - θ)⁻¹

    The finite geometric reference sum is bounded by the full geometric tail: for θ ∈ (0,1) and lengths l ≥ 1, ∑_{l ∈ L} θ^{l-1} ≤ (1 - θ)⁻¹.

    Used by
      theorem

      InformationTheory.Shannon.empirical_entropy_le_log_mean_of_lt

      source
      (L : Finset ℕ) (cf : ℕ → ℝ) (hpos : ∀ l ∈ L, 0 < cf l) (hl1 : ∀ l ∈ L, 1 ≤ l) (hC : 0 < ∑ l ∈ L, cf l) (hCN_lt : ∑ l ∈ L, cf l < ∑ l ∈ L, ↑l * cf l) (hLHS : ∑ l ∈ L, cf l * Real.log ((∑ l ∈ L, cf l) / cf l) = (∑ l ∈ L, cf l) * Real.log (∑ l ∈ L, cf l) - ∑ l ∈ L, cf l * Real.log (cf l)) :
      ∑ l ∈ L, cf l * Real.log ((∑ l ∈ L, cf l) / cf l) ≤ (∑ l ∈ L, cf l) * Real.log ((∑ l ∈ L, ↑l * cf l) / ∑ l ∈ L, cf l) + ∑ l ∈ L, cf l
      Used by
        theorem

        InformationTheory.Shannon.empirical_entropy_le_log_mean

        source
        (L : Finset ℕ) (cf : ℕ → ℝ) (hpos : ∀ l ∈ L, 0 < cf l) (hl1 : ∀ l ∈ L, 1 ≤ l) (hC : 0 < ∑ l ∈ L, cf l) :
        ∑ l ∈ L, cf l * Real.log ((∑ l ∈ L, cf l) / cf l) ≤ (∑ l ∈ L, cf l) * Real.log ((∑ l ∈ L, ↑l * cf l) / ∑ l ∈ L, cf l) + ∑ l ∈ L, cf l

        The empirical-entropy / mean bound (LZ78 overhead crux).

        For a length profile cf : ℕ → ℝ supported on a finite set L of positive lengths (l ≥ 1) with positive counts, writing C = ∑ cf (total count) and N = ∑ l · cf l (total length), the empirical entropy is controlled by the log of the mean length:

        ∑_l cf l · log (C / cf l) ≤ C · log (N / C) + C.

        This is the o(n) overhead estimate: C · log (N / C) scales like C · log(mean length), which is o(n) once the mean is ~ log n.

        Used by