BanditRLProof.LowerBounds.PrefixCodeConstruction

All words at depth n in the full binary tree.

def binaryWords (n : ℕ) : Finset (List Bool)

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

theorem card_binaryWords (n : ℕ) : (binaryWords n).card = 2 ^ n

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

theorem mem_binaryWords_iff (w : List Bool) (n : ℕ) : w ∈ binaryWords n ↔ w.length = n

The descendants of a prefix after n additional bits.

def binaryExtensions (w : List Bool) (n : ℕ) : Finset (List Bool)

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

theorem card_binaryExtensions (w : List Bool) (n : ℕ) : (binaryExtensions w n).card = 2 ^ n

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

theorem mem_binaryExtensions_iff (w v : List Bool) (n : ℕ) : v ∈ binaryExtensions w n ↔ w <+: v ∧ v.length = w.length + n

Cylinders from incomparable prefixes are disjoint.

theorem binaryExtensions_disjoint_of_incomparable (u v : List Bool) (m n : ℕ) (huv : ¬ u <+: v) (hvu : ¬ v <+: u) : Disjoint (binaryExtensions u m) (binaryExtensions v n)

A free word exists whenever previous prefixes occupy fewer than all level nodes.

theorem exists_binaryWord_avoiding_prefixes (S : Finset (List Bool)) (n : ℕ) (hlen : ∀ w ∈ S, w.length ≤ n) (hbudget : (∑ w ∈ S, 2 ^ (n - w.length)) < 2 ^ n) : ∃ v : List Bool, v.length = n ∧ ∀ w ∈ S, ¬ w <+: v

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

theorem binary_level_mul_kraft_weight {k n : ℕ} (h : k ≤ n) : (2 : ℝ) ^ n * (1 / 2 : ℝ) ^ k = 2 ^ (n - k)

Real Kraft slack supplies the integer capacity needed to insert a word.

theorem exists_binaryWord_of_kraft_lt_one (S : Finset (List Bool)) (n : ℕ) (hlen : ∀ w ∈ S, w.length ≤ n) (hk : (∑ w ∈ S, (1 / 2 : ℝ) ^ w.length) < 1) : ∃ v : List Bool, v.length = n ∧ ∀ w ∈ S, ¬ w <+: v

The greedy insertion preserves prefix freedom in both directions.

theorem exists_prefixFree_insert_of_kraft_lt_one (S : Finset (List Bool)) (n : ℕ) (hfree : ∀ a ∈ S, ∀ b ∈ S, a <+: b → a = b) (hlen : ∀ w ∈ S, w.length ≤ n) (hk : (∑ w ∈ S, (1 / 2 : ℝ) ^ w.length) < 1) : ∃ v : List Bool, v.length = n ∧ v ∉ S ∧ ∀ a ∈ insert v S, ∀ b ∈ insert v S, a <+: b → a = b

Finite Kraft converse, retaining each prescribed length, including equality.

theorem exists_prefix_encoding_of_kraft_le_one {α : Type*} [DecidableEq α] (s : Finset α) (l : α → ℕ) (hk : (∑ i ∈ s, (1 / 2 : ℝ) ^ l i) ≤ 1) : ∃ c : α → List Bool, (∀ i ∈ s, (c i).length = l i) ∧ (∀ i ∈ s, ∀ j ∈ s, c i <+: c j → i = j)

Backwards-compatible strict version of the finite Kraft converse.

theorem exists_prefix_encoding_of_kraft_lt_one {α : Type*} [DecidableEq α] (s : Finset α) (l : α → ℕ) (hk : (∑ i ∈ s, (1 / 2 : ℝ) ^ l i) < 1) : ∃ c : α → List Bool, (∀ i ∈ s, (c i).length = l i) ∧ (∀ i ∈ s, ∀ j ∈ s, c i <+: c j → i = j)

Non-strict Kraft converse packaged as an actual binary prefix code.

theorem exists_binaryPrefixCode_of_kraft_le_one {α : Type*} [Fintype α] [DecidableEq α] (l : α → ℕ) (hl : ∀ i, 0 < l i) (hk : (∑ i, (1 / 2 : ℝ) ^ l i) ≤ 1) : ∃ code : BinaryPrefixCode α, ∀ i, (code.encode i).length = l i

Backwards-compatible strict Kraft packaging.

theorem exists_binaryPrefixCode_of_kraft_lt_one {α : Type*} [Fintype α] [DecidableEq α] (l : α → ℕ) (hl : ∀ i, 0 < l i) (hk : (∑ i, (1 / 2 : ℝ) ^ l i) < 1) : ∃ code : BinaryPrefixCode α, ∀ i, (code.encode i).length = l i

Every finite uniquely decodable encoder has a prefix code with exactly the same symbol lengths (the boxed assertion in Chapter 14, Section 14.1).

theorem exists_prefixCode_of_uniquelyDecodable {α : Type*} [Fintype α] (c : α → List Bool) (hinj : Function.Injective c) (hud : InformationTheory.UniquelyDecodable (Set.range c)) : ∃ code : BinaryPrefixCode α, ∀ i, (code.encode i).length = (c i).length

A realizable finite prefix code attains the one-bit entropy sandwich. This proves existence, not Huffman's algorithm or optimality.

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