InformationTheory.Shannon.Huffman.ExpectedLength

Imports 16

Expected length of the Huffman code #

The multiset-level cost huffmanCost aggregates the expected codeword length of huffmanLengthAux. Its merge-step recurrence and dependence only on the probability multiset are the machinery used in the optimality proof; expectedLength_eq_huffmanCost ties it back to the expected length of the published huffmanLength.

Main definitions #

huffmanCost — multiset-level expected length used in the cost-level optimality proof.

Main statements #

huffmanCost_step — huffmanCost decreases by the merged-group probability at each step.
huffmanCost_eq_of_prob_multiset — huffmanCost depends only on the probability multiset.
expectedLength_eq_huffmanCost — the expected length of huffmanLength P equals huffmanCost (initMultiset P).

Cost-level recurrence for the optimality proof #

noncomputable def

InformationTheory.Shannon.Huffman.huffmanCost

source

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

ℝ

Multiset-level expected length ∑_p p.2 * (∑_{a ∈ p.1} huffmanLengthAux s a) / p.1.card. Since depth is constant on each group, this equals ∑_p p.2 * depth(p). @audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanCost_step

source

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

huffmanCost s = huffmanCost (↑(huffmanStep s hs hg)).2.2 + ((↑(huffmanStep s hs hg)).1.2 + (↑(huffmanStep s hs hg)).2.1.2)

huffmanCost s = huffmanCost s'' + (x1.2 + x2.2) where s'' is the merged multiset. @audit:ok

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanCost_eq_zero_of_base

source

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

huffmanCost s = 0

huffmanCost s = 0 when s.card ≤ 1. @audit:ok

Used by

theorem

InformationTheory.Shannon.Huffman.huffmanCost_eq_of_prob_multiset

source

{α : Type u_2} [DecidableEq α] [LinearOrder α] {β : Type u_3} [DecidableEq β] [LinearOrder β] (s : Multiset (Finset α × ℝ)) (t : Multiset (Finset β × ℝ)) (hsg : HuffmanGrouping s) (htg : HuffmanGrouping t) (h : Multiset.map Prod.snd s = Multiset.map Prod.snd t) :

huffmanCost s = huffmanCost t

huffmanCost depends only on the probability multiset s.map Prod.snd. @audit:ok

Used by

theorem

InformationTheory.Shannon.Huffman.expectedLength_eq_huffmanCost

source

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

ShannonCode.expectedLength P (huffmanLength P) = huffmanCost (initMultiset P)

expectedLength P (huffmanLength P) = huffmanCost (initMultiset P). @audit:ok

Used by