InformationTheory

InformationTheory.Shannon.LZ78.ZivLengthGrouping

source

Imports 7

LZ78 length-grouping Jensen inequality #

This file supplies the abstract grouping inequality at the heart of the length-grouping route for the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (LZ78/AsymptoticOptimality/ParentBridgeAchievability.lean).

Approach #

The gateway atom is a pure Finset/Real statement, free of any measure-theoretic or LZ78 content: grouping c = ∑ k i distinct items into D = G.card groups and applying Jensen's inequality to the convex function x ↦ x · log x yields

c · log c ≤ ∑ i, k i · log (k i) + c · log D.

Mathematically this is ConvexOn.map_sum_le for Real.convexOn_mul_log with uniform weights wᵢ = 1/D at points pᵢ = k i: f (c/D) ≤ (1/D) ∑ f (k i), i.e. c · log (c/D) ≤ ∑ k i · log (k i) after multiplying by D, then log (c/D) = log c − log D rearranges to the goal. The degenerate c = 0 case (all k i = 0) is handled directly.

theorem

InformationTheory.Shannon.card_mul_log_le_sum_group_mul_log_add_card_log

source
{ι : Type u_1} (G : Finset ι) (k : ι → ℕ) (hG : G.Nonempty) :
↑(∑ i ∈ G, k i) * Real.log ↑(∑ i ∈ G, k i) ≤ ∑ i ∈ G, ↑(k i) * Real.log ↑(k i) + ↑(∑ i ∈ G, k i) * Real.log ↑G.card

The abstract length-grouping Jensen inequality (gateway atom for the LZ78 length-grouping route). For a nonempty finite index set G and weights k : ι → ℕ, writing c = ∑ i ∈ G, k i and D = G.card,

c · log c ≤ ∑ i ∈ G, k i · log (k i) + c · log D.

This is Jensen's inequality for the convex function x ↦ x · log x with uniform weights 1/D at points k i.

Used by

    Length-grouped instantiation for lz78PhraseStrings #

    theorem

    InformationTheory.Shannon.lz78PhraseStrings_card_mul_log_le_sum_length_group

    source
    {α : Type u_1} [DecidableEq α] (input : List α) :
    have phrases := (lz78PhraseStrings input).toFinset; ↑(lz78PhraseStrings input).length * Real.log ↑(lz78PhraseStrings input).length ≤ ∑ ℓ ∈ Finset.image List.length phrases, ↑{w ∈ phrases | w.length = ℓ}.card * Real.log ↑{w ∈ phrases | w.length = ℓ}.card + ↑(lz78PhraseStrings input).length * Real.log ↑(Finset.image List.length phrases).card

    The length-grouped entropy bound for the LZ78 phrase set, obtained by instantiating the abstract Jensen grouping inequality at the distinct LZ78 phrases, fibered by List.length. With c = #phrases, c_ℓ = #{phrase | length = ℓ} and D = #{distinct lengths},

    c · log c ≤ ∑_ℓ c_ℓ · log c_ℓ + c · log D.

    The phrase set is Nodup (lz78PhraseStrings_nodup), so its toFinset cardinality equals its length, and card_eq_sum_card_image over List.length distributes c across the length fibers.

    Used by