InformationTheory

InformationTheory.Shannon.Huffman.SwapNormCompletion

source

Imports 11

Kraft completion: shorten a feasible code to a complete one #

Main statement #

shorten_to_kraft_one — if ll : β → ℕ is positive with ∑ 2^(-ll x) ≤ 1 and 2 ≤ card β, then there exists l1 ≤ ll (pointwise) with ∑ 2^(-l1 x) = 1.

Implementation notes #

The proof uses a natural-number Kraft sum N(l, M) = ∑ 2^(M - l c) (where M is the maximum codeword length) linked to the real Kraft sum by realKraft = N / 2^M. Induction runs on the total codeword length ∑ ll x: in the Kraft < 1 case, shorten the longest leaf m by 1 (which increments N by 1) and apply the induction hypothesis.

Natural-number Kraft sum vs real Kraft sum #

theorem

InformationTheory.Shannon.Huffman.natKraft_cast_eq

source
{β : Type u_1} [Fintype β] (l : β → ℕ) (M : ℕ) (hM : ∀ (c : β), l c ≤ M) :
↑(∑ c : β, 2 ^ (M - l c)) = 2 ^ M * ∑ c : β, 2 ^ (-↑(l c))

Cast identity: ((∑ c, 2^(M - l c) : ℕ) : ℝ) = 2^M · ∑ c, (2:ℝ)^(-(l c : ℤ)).

Used by
    theorem

    InformationTheory.Shannon.Huffman.realKraft_le_one_iff_nat_le

    source
    {β : Type u_1} [Fintype β] (l : β → ℕ) (M : ℕ) (hM : ∀ (c : β), l c ≤ M) :
    ∑ c : β, 2 ^ (-↑(l c)) ≤ 1 ↔ ∑ c : β, 2 ^ (M - l c) ≤ 2 ^ M

    Equivalence: real Kraft sum ≤ 1 iff natural-number Kraft sum ≤ 2^M (when M bounds l).

    Used by
      theorem

      InformationTheory.Shannon.Huffman.realKraft_eq_one_iff_nat_eq

      source
      {β : Type u_1} [Fintype β] (l : β → ℕ) (M : ℕ) (hM : ∀ (c : β), l c ≤ M) :
      ∑ c : β, 2 ^ (-↑(l c)) = 1 ↔ ∑ c : β, 2 ^ (M - l c) = 2 ^ M

      Equivalence: real Kraft sum = 1 iff natural-number Kraft sum = 2^M (when M bounds l).

      Used by

        Shortening induction #

        theorem

        InformationTheory.Shannon.Huffman.shorten_to_kraft_one

        source
        {β : Type u_1} [Fintype β] [Nonempty β] (ll : β → ℕ) (hll_pos : ∀ (x : β), 0 < ll x) (hll_kraft : ∑ x : β, 2 ^ (-↑(ll x)) ≤ 1) (h_card : 2 ≤ Fintype.card β) :
        ∃ (l1 : β → ℕ), (∀ (x : β), 0 < l1 x) ∧ (∀ (x : β), l1 x ≤ ll x) ∧ ∑ x : β, 2 ^ (-↑(l1 x)) = 1

        A positive Kraft-feasible code can be shortened pointwise to a complete code (Kraft = 1).

        Used by