BanditRLProof.LowerBounds.HuffmanConstruction

No declaration docstring is present; use the chapter context and exact statement below.

theorem oneBitCode_optimal {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (code : BinaryPrefixCode α) (hlen : ∀ i, (code.encode i).length = 1) : IsOptimalPrefixCode p code

No declaration docstring is present; use the chapter context and exact statement below.

def emptyRemainderRoot {α : Type*} [IsEmpty α] : BinaryPrefixCode (α ⊕ Bool) where

Huffman's recursive merge-two-least construction, with its correctness proof. Real-weight choices are classical; the code itself is assembled recursively.

noncomputable def huffmanOptimalCode {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) : {code : BinaryPrefixCode α // IsOptimalPrefixCode p code}

The prefix code produced by recursive Huffman merging.

noncomputable def huffmanCode {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) : BinaryPrefixCode α

No declaration docstring is present; use the chapter context and exact statement below.

theorem huffmanCode_optimal {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) : IsOptimalPrefixCode p (huffmanCode p hp)

Chapter 14, Eq. (14.2), for the recursively constructed Huffman code.

theorem huffmanCode_entropy_sandwich {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength p (huffmanCode p hp) ∧ expectedCodeLength p (huffmanCode p hp) ≤ discreteEntropyBaseTwo Finset.univ p + 1