Skip to content

InformationTheory.Shannon.Huffman.Length

Imports 14

Huffman code lengths #

Constructs the binary Huffman code length function huffmanLength for a finite alphabet α equipped with a probability measure, following Cover–Thomas. This file holds the recursive construction and its positivity invariant; the Kraft sum and the cost-level recurrence live in KraftSum and ExpectedLength.

Main definitions #

groupKey — deterministic comparison key (lex on probability then colex) used to break ties in huffmanStep.
HuffmanGrouping — invariant on the working multiset: no-duplicates, nonempty groups, pairwise-disjoint carriers.
huffmanStep — one merge step: extracts the two minimum-probability groups and returns the merged multiset together with a proof that HuffmanGrouping is preserved.
huffmanLengthAux — recursion on the multiset; assigns a codeword length to each α-element.
initMultiset — initial multiset of singleton groups ({a}, P.real {a}).
huffmanLength — the published codeword-length function huffmanLengthAux (initMultiset P).

Main statements #

groupKey_injective — groupKey is injective (probability + colex breaks all ties).
huffmanStep_min_fst / huffmanStep_min_snd — the two extracted groups have minimum probability in s (resp. s.erase .val.1).
huffmanLength_pos — huffmanLength P a > 0 when card α ≥ 2.

Implementation notes #

The merge step uses groupKey (a lex order on ℝ ×ₗ Colex (Finset α)) rather than a plain probability ordering so that the minimum selection is deterministic even under probability ties. This is essential for the carrier-crossing cost argument (huffmanCost_eq_of_prob_multiset).

noncomputable def

InformationTheory.Shannon.Huffman.groupKey

{α : Type u_1} (p : Finset α × ℝ) :

Lex (ℝ × Colex (Finset α))

Deterministic comparison key for huffmanStep: primary key is probability p.2 (ascending), tie-break is toColex p.1 (colex order). The resulting Prod.Lex total order on ℝ ×ₗ Colex (Finset α) makes the minimum selection unique even under probability ties.

Equations

InformationTheory.Shannon.Huffman.groupKey p = toLex (p.2, toColex p.1)

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.groupKey_injective

{α : Type u_1} :

Function.Injective groupKey

Used by

theorem

InformationTheory.Shannon.Huffman.groupKey_le_imp_snd_le

{α : Type u_1} [LinearOrder α] {p q : Finset α × ℝ} (h : groupKey p ≤ groupKey q) :

p.2 ≤ q.2

Used by

Internal implementation: Multiset-based Huffman recursion #

def

InformationTheory.Shannon.Huffman.HuffmanGrouping

{α : Type u_1} (s : Multiset (Finset α × ℝ)) :

Invariant on a working group multiset: no duplicates, every group is nonempty, and distinct groups have disjoint carriers.

Equations

InformationTheory.Shannon.Huffman.HuffmanGrouping s = (s.Nodup ∧ (∀ p ∈ s, p.1.Nonempty) ∧ ∀ p ∈ s, ∀ q ∈ s, p ≠ q → Disjoint p.1 q.1)

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.HuffmanGrouping.nodup

{α : Type u_1} {s : Multiset (Finset α × ℝ)} (h : HuffmanGrouping s) :

Used by

theorem

InformationTheory.Shannon.Huffman.HuffmanGrouping.nonempty

{α : Type u_1} {s : Multiset (Finset α × ℝ)} (h : HuffmanGrouping s) {p : Finset α × ℝ} (hp : p ∈ s) :

Used by

theorem

InformationTheory.Shannon.Huffman.HuffmanGrouping.disjoint

{α : Type u_1} {s : Multiset (Finset α × ℝ)} (h : HuffmanGrouping s) {p q : Finset α × ℝ} (hp : p ∈ s) (hq : q ∈ s) (hpq : p ≠ q) :

Disjoint p.1 q.1

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanMerged_notMem_eraseErase

{α : Type u_1} [DecidableEq α] {s : Multiset (Finset α × ℝ)} (hg : HuffmanGrouping s) {x1 x2 : Finset α × ℝ} (hx1_mem : x1 ∈ s) (hx2_mem_s : x2 ∈ s) (hx12_ne : x1 ≠ x2) :

(x1.1 ∪ x2.1, x1.2 + x2.2) ∉ (s.erase x1).erase x2

Used by

theorem

InformationTheory.Shannon.Huffman.kraftTerm_of_const_depth

{α : Type u_1} {g : Finset α} (hg_ne : g.Nonempty) (f : α → ℤ) (d : ℤ) (hconst : ∀ a ∈ g, f a = d) :

(∑ a ∈ g, 2 ^ (-f a)) / ↑g.card = 2 ^ (-d)

Used by

noncomputable def

InformationTheory.Shannon.Huffman.huffmanStep

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

{ p : (Finset α × ℝ) × (Finset α × ℝ) × Multiset (Finset α × ℝ) // p.1 ∈ s ∧ p.2.1 ∈ s.erase p.1 ∧ p.2.2 = (p.1.1 ∪ p.2.1.1, p.1.2 + p.2.1.2) ::ₘ (s.erase p.1).erase p.2.1 ∧ HuffmanGrouping p.2.2 }

One Huffman merge step: extracts the two minimum-groupKey groups from s and returns the merged multiset together with membership witnesses and the proof that HuffmanGrouping is preserved. Requires s.card ≥ 2 and HuffmanGrouping s.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_spec

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

(↑(huffmanStep s hs hg)).1 ∈ s ∧ (↑(huffmanStep s hs hg)).2.1 ∈ s.erase (↑(huffmanStep s hs hg)).1 ∧ (↑(huffmanStep s hs hg)).2.2 = ((↑(huffmanStep s hs hg)).1.1 ∪ (↑(huffmanStep s hs hg)).2.1.1, (↑(huffmanStep s hs hg)).1.2 + (↑(huffmanStep s hs hg)).2.1.2) ::ₘ (s.erase (↑(huffmanStep s hs hg)).1).erase (↑(huffmanStep s hs hg)).2.1 ∧ HuffmanGrouping (↑(huffmanStep s hs hg)).2.2

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_key_min_fst

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) (z : Finset α × ℝ) :

z ∈ s → groupKey (↑(huffmanStep s hs hg)).1 ≤ groupKey z

.val.1 minimizes groupKey over all of s.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_min_fst

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) (z : Finset α × ℝ) :

z ∈ s → (↑(huffmanStep s hs hg)).1.2 ≤ z.2

.val.1 has minimum probability in s.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_key_min_snd

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) (z : Finset α × ℝ) :

z ∈ s.erase (↑(huffmanStep s hs hg)).1 → groupKey (↑(huffmanStep s hs hg)).2.1 ≤ groupKey z

.val.2.1 minimizes groupKey over s.erase .val.1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_min_snd

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) (z : Finset α × ℝ) :

z ∈ s.erase (↑(huffmanStep s hs hg)).1 → (↑(huffmanStep s hs hg)).2.1.2 ≤ z.2

.val.2.1 has minimum probability in s.erase .val.1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_grouping

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

HuffmanGrouping (↑(huffmanStep s hs hg)).2.2

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_card_eq

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

(↑(huffmanStep s hs hg)).2.2.card = s.card - 1

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_card_lt

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

(↑(huffmanStep s hs hg)).2.2.card < s.card

Used by

noncomputable def

InformationTheory.Shannon.Huffman.huffmanLengthAux

@[irreducible]

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) :

α → ℕ

Internal recursion on s.card: assigns a codeword length to each α-element by strong induction on s.card, merging the two minimum-probability groups at each step. Returns the zero function on out-of-spec inputs (where HuffmanGrouping s fails).

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Huffman.initMultiset

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : MeasureTheory.Measure α) :

Multiset (Finset α × ℝ)

Initial working multiset: each element a : α maps to the singleton group ({a}, P.real {a}).

Equations

InformationTheory.Shannon.Huffman.initMultiset P = Multiset.map (fun (a : α) => ({a}, P.real {a})) Finset.univ.val

Instances For

Used by

Unfolding lemmas and structural invariants for `huffmanLengthAux` #

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_eq_step

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (h : 2 ≤ s.card) (hg : HuffmanGrouping s) :

huffmanLengthAux s = have step := ↑(huffmanStep s h hg); have A := step.1.1; have B := step.2.1.1; have s'' := step.2.2; have g := huffmanLengthAux s''; fun (a : α) => if a ∈ A ∨ a ∈ B then g a + 1 else g a

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_eq_zero

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (h : s.card ≤ 1) (hg : HuffmanGrouping s) :

huffmanLengthAux s = fun (x : α) => 0

Used by

Main definition #

noncomputable def

InformationTheory.Shannon.Huffman.huffmanLength

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [MeasurableSpace α] (P : MeasureTheory.Measure α) :

α → ℕ

Binary Huffman codeword-length function: huffmanLengthAux applied to the initial singleton-group multiset of P.

Equations

InformationTheory.Shannon.Huffman.huffmanLength P = InformationTheory.Shannon.Huffman.huffmanLengthAux (InformationTheory.Shannon.Huffman.initMultiset P)

Instances For

Used by

Main theorems #

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_pos_of_mem

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (a : α) (hmem : ∃ p ∈ s, a ∈ p.1) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) :

0 < huffmanLengthAux s a

Used by

theorem

InformationTheory.Shannon.Huffman.mem_initMultiset

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : MeasureTheory.Measure α) (a : α) :

∃ p ∈ initMultiset P, a ∈ p.1

Used by

theorem

InformationTheory.Shannon.Huffman.initMultiset_huffmanGrouping

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : MeasureTheory.Measure α) :

HuffmanGrouping (initMultiset P)

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_pos

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [MeasurableSpace α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (_hP : ∀ (a : α), 0 < P.real {a}) (h_card : 2 ≤ Fintype.card α) (a : α) :

0 < huffmanLength P a

huffmanLength P a > 0 when Fintype.card α ≥ 2.

Used by