BanditRLProof.LowerBounds.HuffmanAlphabet

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

theorem expectedCodeLength_relabel {α β : Type*} [Fintype α] [Fintype β] (p : α → ℝ) (code : BinaryPrefixCode α) (e : β ≃ α) : expectedCodeLength (p ∘ e) (code.relabel e) = expectedCodeLength p code

Global optimality is independent of the names of the alphabet symbols.

theorem IsOptimalPrefixCode.relabel {α β : Type*} [Fintype α] [Fintype β] (p : α → ℝ) (code : BinaryPrefixCode α) (e : β ≃ α) (hopt : IsOptimalPrefixCode p code) : IsOptimalPrefixCode (p ∘ e) (code.relabel e)

The unmerged symbols, retaining their original labels.

def HuffmanRemainder {α : Type*} (a b : α)

Separate two selected symbols as the false and true leaves.

def huffmanSplitEquiv {α : Type*} [DecidableEq α] (a b : α) (hab : a ≠ b) : HuffmanRemainder a b ⊕ Bool ≃ α where

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

@[simp] theorem huffmanSplitEquiv_false {α : Type*} [DecidableEq α] (a b : α) (hab : a ≠ b) : huffmanSplitEquiv a b hab (.inr false) = a

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

@[simp] theorem huffmanSplitEquiv_true {α : Type*} [DecidableEq α] (a b : α) (hab : a ≠ b) : huffmanSplitEquiv a b hab (.inr true) = b

Merging two distinct symbols reduces the recursive alphabet size by one.

theorem huffman_merged_card_lt {α : Type*} [Fintype α] [DecidableEq α] (a b : α) (hab : a ≠ b) : Fintype.card (Option (HuffmanRemainder a b)) < Fintype.card α

A finite nontrivial alphabet has two least weights, including ties.

theorem exists_two_least_weights {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] (p : α → ℝ) : ∃ a b, a ≠ b ∧ (∀ i, p a ≤ p i) ∧ (∀ i, i ≠ a → p b ≤ p i)