InformationTheory

InformationTheory.Shannon.McMillanKraftBridge

source

Imports 5

McMillan → Kraft → Gibbs converse bridge (symbol-code level) #

This file wires Mathlib's InformationTheory.kraft_mcmillan_inequality (uniquely-decodable code ⟹ ∑ D^{-|w|} ≤ 1, a counting theorem in Mathlib/InformationTheory/Coding/KraftMcMillan.lean) into this project's per-symbol Kraft / Gibbs framework (InformationTheory/Shannon/ShannonCode/Basic.lean). McMillan itself is not reproved here; this file is a bridge, not a re-derivation.

The result is an expectation-level source-coding converse (Cover–Thomas): for any finite-alphabet source P whose codeword assignment c : α → List β is injective with a uniquely-decodable image, the entropy lower-bounds the expected code length,

H_D(P) ≤ E[L]    where  D = |β|,  L a = |c a|.

Beyond McMillan and the project's Gibbs bound entropyD_le_expectedLength_of_kraft, the only hypotheses are the regularity preconditions of a code: full support of P, 1 < D, injectivity of c, and unique decodability of its image.

Relation to the LZ78 converse #

The phrase-string set lz78PhraseStrings is not a McMillan code: the LZ78 dictionary is prefix-complete (lz78PhraseStringsAux extends cur ++ [s] only while cur is already an entry), so [a] and [a, b] can both be entries and the set is far from prefix-free. lz78PhraseStrings_nodup gives distinctness, which is necessary but not sufficient for UniquelyDecodable. The uniquely-decodable object in LZ78 is the encoded (parent index, symbol) token stream, constructed in LZ78/ConverseUDObject.lean, which feeds it back through §2 to obtain kraftSum ≤ 1 and entropyD 2 P ≤ E[L] for the token code.

That is still an expectation-level bound, whereas the LZ78 converse is the a.s.-eventual, per-realization inequality

∀ᵐ ω, ∀ᶠ n,  blockLogAvg₂ μ p n ω − err n ≤ lz n (block_n ω) / n

with err n → 0. The averaged bound does not imply it: for a fixed realization an LZ78 codeword can be shorter than −log₂ Pₙ{x}, which is precisely the universality of LZ78. The lift is the Barron / competitive-optimality argument (a polynomial n-block Kraft bound plus Borel–Cantelli), and it does not run through this file; it lives in LZ78/AsymptoticOptimality/ParentBridgeConverse.lean (lz78_block_kraft_poly, blockLogAvg₂_minus_error_le_rate_ae, lz78Greedy_converse_ae).

File layout #

§1. Rewriting kraftSum into the McMillan weight shape #

theorem

InformationTheory.Shannon.ShannonCode.zpow_neg_natCast_eq_one_div_pow

source
(D : ℝ) (n : ℕ) :
D ^ (-↑n) = (1 / D) ^ n

D ^ (-(n : ℤ)) = (1 / D) ^ n for any real D (McMillan uses the (1/D)^{|w|} weight; the project's kraftSum uses D ^ (-(l a : ℤ))).

Used by
    theorem

    InformationTheory.Shannon.ShannonCode.kraftSum_eq_sum_one_div_pow

    source
    {α : Type u_1} [Fintype α] (D : ℝ) (l : α → ℕ) :
    kraftSum D l = ∑ a : α, (1 / D) ^ l a

    kraftSum D l = ∑ a, (1/D) ^ (l a) — the McMillan-weight rewriting of the project's kraftSum.

    Used by

      §2. McMillan ⟹ kraftSum ≤ 1 ⟹ Gibbs converse #

      theorem

      InformationTheory.Shannon.ShannonCode.kraftSum_le_one_of_uniquelyDecodable

      source
      {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] [Nonempty β] [DecidableEq β] (c : α → List β) (hc : Function.Injective c) (hUD : UniquelyDecodable ↑(Finset.image c Finset.univ)) :
      (kraftSum ↑(Fintype.card β) fun (a : α) => (c a).length) ≤ 1

      McMillan's inequality, per-symbol form: if the codeword assignment c : α → List β is injective with uniquely-decodable image, then the per-symbol Kraft sum kraftSum |β| (|c ·|) ≤ 1.

      D = Fintype.card β is the alphabet size; the codeword lengths are l a = (c a).length. The image c '' univ is a finite set of distinct codewords; McMillan's kraft_mcmillan_inequality gives ∑_{w ∈ image} (1/|β|)^{|w|} ≤ 1, and reindexing by the injective c recovers the per-symbol sum.

      Used by
        theorem

        InformationTheory.Shannon.ShannonCode.entropyD_le_expectedLength_of_uniquelyDecodable

        source
        {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_2} [Fintype β] [Nonempty β] [DecidableEq β] (hD : 1 < ↑(Fintype.card β)) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) (c : α → List β) (hc : Function.Injective c) (hUD : UniquelyDecodable ↑(Finset.image c Finset.univ)) :
        entropyD (↑(Fintype.card β)) P ≤ expectedLength P fun (a : α) => (c a).length

        The expectation-level source-coding converse from McMillan.

        For a finite-alphabet source P (full support) and an injective codeword assignment c : α → List β whose image is uniquely-decodable, the D-ary entropy lower-bounds the expected code length:

        H_D(P) ≤ E[L],   D = |β|,  L a = |c a|.

        It composes McMillan (Kraft) with entropyD_le_expectedLength_of_kraft (Gibbs). The full-support hypothesis is a regularity precondition: it makes the logb arguments positive.

        A note on D > 1: the Gibbs lemma needs 1 < D = |β|, i.e. at least a binary alphabet. With a unary alphabet (|β| = 1) no uniquely-decodable code of more than one nonempty word exists, so the hypothesis is the natural one.

        Used by