InformationTheory.Shannon.Huffman.KraftSum

Imports 15

Kraft inequality for Huffman code lengths #

The Kraft sum of the Huffman codeword-length function equals 1 exactly, hence the lengths satisfy the binary Kraft inequality and a prefix-free code realising them exists. The auxiliary constancy lemma huffmanLengthAux_const_on_group (depth is constant on each group) is shared with the cost-level recurrence in ExpectedLength.

Main statements #

huffmanLength_kraft_eq_one — the Kraft sum equals 1 exactly.
huffmanLength_kraft_le_one — the Kraft inequality holds.
exists_huffman_prefix_code — a prefix-free binary code of the Huffman lengths exists.

Kraft inequality: auxiliary lemmas (constancy and invariants) #

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_const_on_group

source

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hg : HuffmanGrouping s) (p : Finset α × ℝ) (hp : p ∈ s) (a b : α) (ha : a ∈ p.1) (hb : b ∈ p.1) :

huffmanLengthAux s a = huffmanLengthAux s b

Used by

noncomputable def

InformationTheory.Shannon.Huffman.kraftPerGroup

source

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

ℝ

Per-group Kraft sum: ∑_p (∑_{a ∈ p.1} 2^(-huffmanLengthAux s a)) / p.1.card. By huffmanLengthAux_const_on_group this equals ∑_p 2^(-depth(p)).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.kraftPerGroup_eq_card_of_base

source

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

kraftPerGroup s = ↑s.card

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanStep_orig_decomp

source

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

s = (↑(huffmanStep s hs hg)).1 ::ₘ (↑(huffmanStep s hs hg)).2.1 ::ₘ (s.erase (↑(huffmanStep s hs hg)).1).erase (↑(huffmanStep s hs hg)).2.1

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_step_merged

source

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) {a : α} (ha : a ∈ (↑(huffmanStep s hs hg)).1.1 ∨ a ∈ (↑(huffmanStep s hs hg)).2.1.1) :

huffmanLengthAux s a = huffmanLengthAux (↑(huffmanStep s hs hg)).2.2 a + 1

huffmanLengthAux s a = huffmanLengthAux s'' a + 1 for a ∈ x1.1 ∪ x2.1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_step_other

source

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) {a : α} (ha : ¬(a ∈ (↑(huffmanStep s hs hg)).1.1 ∨ a ∈ (↑(huffmanStep s hs hg)).2.1.1)) :

huffmanLengthAux s a = huffmanLengthAux (↑(huffmanStep s hs hg)).2.2 a

huffmanLengthAux s a = huffmanLengthAux s'' a for a ∉ x1.1 ∪ x2.1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLengthAux_step_eq_on_other_group

source

{α : Type u_1} [DecidableEq α] [LinearOrder α] (s : Multiset (Finset α × ℝ)) (hs : 2 ≤ s.card) (hg : HuffmanGrouping s) (q : Finset α × ℝ) (hq : q ∈ (s.erase (↑(huffmanStep s hs hg)).1).erase (↑(huffmanStep s hs hg)).2.1) {a : α} (ha : a ∈ q.1) :

huffmanLengthAux s a = huffmanLengthAux (↑(huffmanStep s hs hg)).2.2 a

Used by

theorem

InformationTheory.Shannon.Huffman.kraftPerGroup_step

source

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

kraftPerGroup s = kraftPerGroup (↑(huffmanStep s hs hg)).2.2

Used by

theorem

InformationTheory.Shannon.Huffman.kraftPerGroup_eq_one

source

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

kraftPerGroup s = 1

Used by

theorem

InformationTheory.Shannon.Huffman.kraftPerGroup_initMultiset_eq_kraft

source

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

kraftPerGroup (initMultiset P) = ∑ a : α, 2 ^ (-↑(huffmanLength P a))

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_kraft_eq_one

source

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

∑ a : α, 2 ^ (-↑(huffmanLength P a)) = 1

The Kraft sum of huffmanLength P equals 1.

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanLength_kraft_le_one

source

{α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] [Nonempty α] [MeasurableSpace α] (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) :

∑ a : α, 2 ^ (-↑(huffmanLength P a)) ≤ 1

huffmanLength P satisfies the binary Kraft inequality (in fact with equality).

Used by

theorem

InformationTheory.Shannon.Huffman.exists_huffman_prefix_code

source

∃ (c : α → List (Fin 2)), Function.Injective c ∧ (∀ (a : α), (c a).length = huffmanLength P a) ∧ ShannonCodeKraftReverse.IsPrefixFree c

A prefix-free binary code realising the huffmanLength P exists.

Used by