InformationTheory

InformationTheory.Shannon.Huffman.StrongForm

source

Imports 5

Swap normalization and Huffman optimality (Cover–Thomas) #

Provides the constructive proof that SwapNormalizationHypothesis holds (swap_normalization_proof), and thereby establishes the unconditional optimality theorem huffmanLength_optimal.

Main statements #

  • swap_normalization_strong — given a Kraft-feasible ll and the two minimum-probability elements (a, b) (a = global-min, b = second-min), there exists l_norm with l_norm a = l_norm b, Kraft ≤ 1, and expected length ≤ that of ll.
  • swap_normalization_proof — discharges SwapNormalizationHypothesis unconditionally.
  • huffmanLength_optimal — Huffman's theorem: huffmanLength P is optimal among all Kraft-feasible length functions.

Implementation notes #

The swap normalization proof proceeds in three steps:

  1. Shorten ll to a complete code l1 (Kraft = 1) via shorten_to_kraft_one.
  2. Find two equal-longest leaves c₁ ≠ c₂ of l1 via exists_two_equal_longest.
  3. Swap a ↔ c₁ then b ↔ c₂ using swap_step_le, so that l_norm a = l_norm b = L.

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
theorem

InformationTheory.Shannon.Huffman.swap_normalization_strong

source
{β : Type u} [Fintype β] [LinearOrder β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (Q : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure Q] (ll : β → ℕ) (hll_pos : ∀ (x : β), 0 < ll x) (hll_kraft : ∑ x : β, 2 ^ (-↑(ll x)) ≤ 1) (a b : β) (hab : a ≠ b) (h_a_min : ∀ (c : β), Q.real {a} ≤ Q.real {c}) (h_b_min : ∀ (c : β), c ≠ a → Q.real {b} ≤ Q.real {c}) (h_card : 3 ≤ Fintype.card β) :
∃ (l_norm : β → ℕ), (∀ (x : β), 0 < l_norm x) ∧ ∑ x : β, 2 ^ (-↑(l_norm x)) ≤ 1 ∧ l_norm a = l_norm b ∧ ShannonCode.expectedLength Q l_norm ≤ ShannonCode.expectedLength Q ll

Constructive core of swap normalization: given Kraft-feasible ll and minimum-probability pair (a, b) (a = global-min, b = second-min), produces l_norm satisfying l_norm a = l_norm b, Kraft ≤ 1, positive, and expectedLength Q l_norm ≤ expectedLength Q ll.

Used by

    Unconditional Huffman optimality #

    theorem

    InformationTheory.Shannon.Huffman.swap_normalization_proof

    source
    :
    SwapNormalizationHypothesis
    Used by
      theorem

      InformationTheory.Shannon.Huffman.huffmanLength_optimal

      source
      {α : Type u} [Fintype α] [DecidableEq α] [LinearOrder α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) (l : α → ℕ) (hl_pos : ∀ (a : α), 0 < l a) (hl_kraft : ∑ a : α, 2 ^ (-↑(l a)) ≤ 1) :
      ShannonCode.expectedLength P (huffmanLength P) ≤ ShannonCode.expectedLength P l

      Huffman's theorem (optimality): huffmanLength P minimizes expected codeword length among all positive Kraft-feasible length functions. @audit:ok

      Used by