Skip to content

InformationTheory.Shannon.Huffman.Optimality

Imports 12

Huffman optimality — Cover–Thomas #

Proves that huffmanLength minimizes expected codeword length among all Kraft-feasible length functions, via the sibling property and n → n-1 strong induction.

Main statements #

exists_deepest_leaf — a deepest leaf of huffmanLength P always exists.
exists_sibling_min_pair — the sibling property: the two minimum-probability elements have equal Huffman length.
huffmanLength_optimal_aux — induction motor: huffmanLength P is optimal among Kraft-feasible length functions, given swap normalization as a hypothesis.

Implementation notes #

The proof uses a hybrid design: the merged alphabet is α' := { x : α // x ≠ b } (a Subtype), and mergedMeasure assigns probability P{a} + P{b} to the merged element and P{x} elsewhere. mergedMeasure is constructed as Measure.sum (fun x => f x • Measure.dirac x) so that Measure.sum_smul_dirac_singleton applies directly. The induction step avoids a per-symbol depth identity (which would be false for a general Huffman tree) and instead uses the cost-level equality expectedLength_merged_cost_bridge.

References #

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

Deepest leaf and sibling property helpers #

theorem

InformationTheory.Shannon.Huffman.exists_deepest_leaf

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [Nonempty α] [MeasurableSpace α] (P : MeasureTheory.Measure α) (_h_card : 1 ≤ Fintype.card α) :

∃ (a : α), ∀ (c : α), huffmanLength P c ≤ huffmanLength P a

A deepest leaf of huffmanLength P exists when Fintype.card α ≥ 1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_eq_of_min_prob_pair

{α : 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 : α) (b : α), a ≠ b ∧ huffmanLength P a = huffmanLength P b ∧ (∀ (c : α), P.real {a} ≤ P.real {c}) ∧ ∀ (c : α), c ≠ a → P.real {b} ≤ P.real {c}

Used by

Sibling property #

theorem

InformationTheory.Shannon.Huffman.exists_sibling_min_pair

{α : 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 : α) (b : α), a ≠ b ∧ huffmanLength P a = huffmanLength P b ∧ (∀ (c : α), P.real {a} ≤ P.real {c}) ∧ ∀ (c : α), c ≠ a → P.real {b} ≤ P.real {c}

Sibling property: the two minimum-probability elements have equal huffmanLength. Returns a = global-min probability and b = second-min probability.

Used by

Merged measure on the reduced alphabet #

noncomputable def

InformationTheory.Shannon.Huffman.mergedMeasure

{α : Type u_1} [DecidableEq α] [MeasurableSpace α] (P : MeasureTheory.Measure α) (a b : α) (_hab : a ≠ b) :

MeasureTheory.Measure { x : α // x ≠ b }

Merged probability measure on α' := { x : α // x ≠ b }: assigns P{a} + P{b} to the merged element and P{x} to all other elements.

Equations

InformationTheory.Shannon.Huffman.mergedMeasure P a b _hab = MeasureTheory.Measure.sum fun (x : { x : α // x ≠ b }) => (if ↑x = a then P {a} + P {b} else P {↑x}) • MeasureTheory.Measure.dirac x

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.mergedMeasure_real

{α : Type u_1} [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure P] (a b : α) (hab : a ≠ b) (x : { x : α // x ≠ b }) :

(mergedMeasure P a b hab).real {x} = if ↑x = a then P.real {a} + P.real {b} else P.real {↑x}

Used by

theorem

InformationTheory.Shannon.Huffman.kraft_sum_mergedLength_eq

{α : Type u_1} [Fintype α] [DecidableEq α] (l : α → ℕ) (hl_pos : ∀ (a : α), 0 < l a) (a b : α) (hab : a ≠ b) (h_lab : l a = l b) :

∑ x : { x : α // x ≠ b }, 2 ^ (-↑(if ↑x = a then l a - 1 else l ↑x)) = ∑ x : α, 2 ^ (-↑(l x))

Used by

theorem

InformationTheory.Shannon.Huffman.expectedLength_eq_mergedMeasure_mergedLength_add

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure P] (l : α → ℕ) (hl_pos : ∀ (a : α), 0 < l a) (a b : α) (hab : a ≠ b) (h_lab : l a = l b) :

ShannonCode.expectedLength P l = (ShannonCode.expectedLength (mergedMeasure P a b hab) fun (x : { x : α // x ≠ b }) => if ↑x = a then l a - 1 else l ↑x) + (P.real {a} + P.real {b})

Used by

theorem

InformationTheory.Shannon.Huffman.expectedLength_bridge_R

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (l : α → ℕ) (hl_pos : ∀ (a : α), 0 < l a) (a b : α) (hab : a ≠ b) (h_lab : l a = l b) (h_la_ge_2 : 2 ≤ l a) (hl_kraft : ∑ x : α, 2 ^ (-↑(l x)) ≤ 1) :

∃ (l' : { x : α // x ≠ b } → ℕ), (∀ (x : { x : α // x ≠ b }), 0 < l' x) ∧ ∑ x : { x : α // x ≠ b }, 2 ^ (-↑(l' x)) ≤ 1 ∧ ShannonCode.expectedLength P l = ShannonCode.expectedLength (mergedMeasure P a b hab) l' + (P.real {a} + P.real {b})

Used by

Probability measure instances for `mergedMeasure` #

theorem

InformationTheory.Shannon.Huffman.mergedMeasure_isProbabilityMeasure

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (a b : α) (hab : a ≠ b) :

MeasureTheory.IsProbabilityMeasure (mergedMeasure P a b hab)

mergedMeasure P a b hab is a probability measure (since P is and the singleton masses sum to 1 on α').

Used by

theorem

InformationTheory.Shannon.Huffman.mergedMeasure_pos

{α : Type u_1} [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) (a b : α) (hab : a ≠ b) (x : { y : α // y ≠ b }) :

0 < (mergedMeasure P a b hab).real {x}

Positivity of mergedMeasure on singletons (from positivity of P).

Used by

theorem

InformationTheory.Shannon.Huffman.swap_step_le

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (l : α → ℕ) (hl_pos : ∀ (x : α), 0 < l x) (hl_kraft : ∑ x : α, 2 ^ (-↑(l x)) ≤ 1) (a m : α) (h_la_le_lm : l a ≤ l m) (h_Pa_le_Pm : P.real {a} ≤ P.real {m}) :

have l' := l ∘ ⇑(Equiv.swap a m); (∀ (x : α), 0 < l' x) ∧ ∑ x : α, 2 ^ (-↑(l' x)) ≤ 1 ∧ ShannonCode.expectedLength P l' ≤ ShannonCode.expectedLength P l ∧ l' a = l m ∧ l' m = l a

Used by

Swap normalization hypothesis #

abbrev

InformationTheory.Shannon.Huffman.SwapNormalizationHypothesis

@[reducible, inline]

:

Interface predicate for the swap normalization step used by huffmanLength_optimal_aux. Given least-prob pair (a, b) with a = global-min and b = second-min, any Kraft-feasible ll can be normalized to l_norm with l_norm a = l_norm b, non-increasing expected length, and Kraft ≤ 1. The constructive proof is swap_normalization_proof in StrongForm.lean.

Equations

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

Instances For

Used by

Cost-level bridge #

theorem

InformationTheory.Shannon.Huffman.initMultiset_mergedMeasure_snd_map_eq

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure P] (a b : α) (hab : a ≠ b) :

Multiset.map Prod.snd (initMultiset (mergedMeasure P a b hab)) = (P.real {a} + P.real {b}) ::ₘ Multiset.map (fun (c : α) => P.real {c}) ((Finset.univ.erase a).erase b).val

Used by

theorem

InformationTheory.Shannon.Huffman.expectedLength_merged_cost_bridge

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (_hP : ∀ (a : α), 0 < P.real {a}) (h_card : 2 ≤ Fintype.card α) (a b : α) (hab : a ≠ b) (h_a_min : ∀ (c : α), P.real {a} ≤ P.real {c}) (h_b_min : ∀ (c : α), c ≠ a → P.real {b} ≤ P.real {c}) :

ShannonCode.expectedLength P (huffmanLength P) = ShannonCode.expectedLength (mergedMeasure P a b hab) (huffmanLength (mergedMeasure P a b hab)) + (P.real {a} + P.real {b})

Cost-level bridge: expectedLength P (huffmanLength P) = expectedLength (mergedMeasure P a b hab) (huffmanLength (mergedMeasure P a b hab)) + (P.real {a} + P.real {b}). @audit:ok

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_le_one_of_card_le_two

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [MeasurableSpace α] (P : MeasureTheory.Measure α) (h_card : Fintype.card α ≤ 2) (x : α) :

huffmanLength P x ≤ 1

Used by

theorem

InformationTheory.Shannon.Huffman.two_le_normalizedLength_of_card_ge_three

{α : Type u_1} [Fintype α] [DecidableEq α] (l_norm : α → ℕ) (hln_pos : ∀ (a : α), 0 < l_norm a) (a b : α) (hab : a ≠ b) (hln_eq_ab : l_norm a = l_norm b) (hln_kraft : ∑ x : α, 2 ^ (-↑(l_norm x)) ≤ 1) (h_card_ge_3 : 3 ≤ Fintype.card α) :

2 ≤ l_norm a

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_optimal_aux

(n : ℕ) (h_swap : SwapNormalizationHypothesis) {α : 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) (hn : Fintype.card α = n) :

ShannonCode.expectedLength P (huffmanLength P) ≤ ShannonCode.expectedLength P l

Strong-induction motor for Huffman optimality. Takes h_swap : SwapNormalizationHypothesis as an argument; the headline huffmanLength_optimal in StrongForm.lean supplies swap_normalization_proof to discharge it unconditionally. @audit:ok

Used by