InformationTheory.Shannon.Huffman.SwapNormProof

Imports 12

The pairing keystone of swap normalization #

If l : β → ℕ is positive and satisfies the binary Kraft equality ∑ c, (2:ℝ)^(-(l c)) = 1, then the maximum codeword length is attained by at least two distinct symbols; equivalently, there is no unique longest leaf.

Implementation notes #

The argument is a parity one: scaling the Kraft equality by 2^M (where M is the max length) turns it into the natural-number identity ∑ c, 2^(M - l c) = 2^M. If the max were unique at b, the sum would be 1 + (even), i.e. odd, contradicting 2^M even.

theorem

InformationTheory.Shannon.Huffman.kraft_one_nat_sum

source

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

∑ c : β, 2 ^ (M - l c) = 2 ^ M

Natural-number form of the Kraft equality. If l is positive, M bounds every l c (∀ c, l c ≤ M), and the real binary Kraft sum equals 1, then the rescaled natural-number sum ∑ c, 2^(M - l c) equals 2^M.

Used by

theorem

InformationTheory.Shannon.Huffman.strict_kraft_one_implies_pairing

source

{β : Type u_1} [Fintype β] (l : β → ℕ) (hl_pos : ∀ (c : β), 0 < l c) (hkraft : ∑ c : β, 2 ^ (-↑(l c)) = 1) (b : β) (hb_max : ∀ (c : β), l c ≤ l b) :

∃ (c : β), c ≠ b ∧ l b ≤ l c

Keystone: Kraft = 1 forbids a unique longest leaf. If l is positive on a Fintype and the binary Kraft sum is exactly 1, then for every b there exists a distinct c ≠ b with l b ≤ l c. In particular the maximum length is attained by at least two symbols.

Used by

theorem

InformationTheory.Shannon.Huffman.exists_two_equal_longest

source

{β : Type u_1} [Fintype β] [Nonempty β] (l : β → ℕ) (hl_pos : ∀ (c : β), 0 < l c) (hkraft : ∑ c : β, 2 ^ (-↑(l c)) = 1) :

∃ (c₁ : β) (c₂ : β), c₁ ≠ c₂ ∧ (∀ (d : β), l d ≤ l c₁) ∧ l c₁ = l c₂

Corollary: a complete (Kraft = 1) binary code has two equal-longest leaves. For a positive length function whose binary Kraft sum is exactly 1, the maximum codeword length is attained by two distinct symbols. This is the structural fact Cover–Thomas uses to argue that the two longest leaves of an optimal binary code are siblings.

Used by