BanditRLProof.LowerBounds.PrefixCodePruning

A deepest leaf with no sibling has a parent incomparable with every other word.

theorem deepest_parent_incomparable {α : Type*} (code : BinaryPrefixCode α) (a : α) (w : List Bool) (b : Bool) (ha : code.encode a = w ++ [b]) (hmax : ∀ i, (code.encode i).length ≤ (code.encode a).length) (hmissing : ∀ i, code.encode i ≠ w ++ [!b]) : ∀ i, i ≠ a → (¬ code.encode i <+: w) ∧ (¬ w <+: code.encode i)

Replace one word by an incomparable nonempty word, preserving code validity.

def BinaryPrefixCode.replaceWord {α : Type*} [DecidableEq α] (code : BinaryPrefixCode α) (a : α) (w : List Bool) (hw : w ≠ []) (hsep : ∀ i, i ≠ a → (¬ code.encode i <+: w) ∧ (¬ w <+: code.encode i)) : BinaryPrefixCode α

Legal deletion of the last bit of a deepest sibling-free leaf.

def BinaryPrefixCode.pruneDeepest {α : Type*} [DecidableEq α] (code : BinaryPrefixCode α) (a : α) (w : List Bool) (b : Bool) (hw : w ≠ []) (ha : code.encode a = w ++ [b]) (hmax : ∀ i, (code.encode i).length ≤ (code.encode a).length) (hmissing : ∀ i, code.encode i ≠ w ++ [!b]) : BinaryPrefixCode α

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

theorem expectedCodeLength_replaceWord {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a : α) (w : List Bool) (hw : w ≠ []) (hsep : ∀ i, i ≠ a → (¬ code.encode i <+: w) ∧ (¬ w <+: code.encode i)) : expectedCodeLength p (code.replaceWord a w hw hsep) = expectedCodeLength p code + p a * (w.length - (code.encode a).length : ℝ)

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

theorem expectedCodeLength_pruneDeepest {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a : α) (w : List Bool) (b : Bool) (hw : w ≠ []) (ha : code.encode a = w ++ [b]) (hmax : ∀ i, (code.encode i).length ≤ (code.encode a).length) (hmissing : ∀ i, code.encode i ≠ w ++ [!b]) : expectedCodeLength p (code.pruneDeepest a w b hw ha hmax hmissing) = expectedCodeLength p code - p a

Pruning remains cost-nonincreasing when the removed symbol has zero mass.

theorem expectedCodeLength_pruneDeepest_le {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a : α) (w : List Bool) (b : Bool) (hp : 0 ≤ p a) (hw : w ≠ []) (ha : code.encode a = w ++ [b]) (hmax : ∀ i, (code.encode i).length ≤ (code.encode a).length) (hmissing : ∀ i, code.encode i ≠ w ++ [!b]) : expectedCodeLength p (code.pruneDeepest a w b hw ha hmax hmissing) ≤ expectedCodeLength p code

Structural termination measure, independent of source probabilities.

def totalCodeLength {α : Type*} [Fintype α] (code : BinaryPrefixCode α) : ℕ

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

theorem totalCodeLength_pruneDeepest {α : Type*} [Fintype α] [DecidableEq α] (code : BinaryPrefixCode α) (a : α) (w : List Bool) (b : Bool) (hw : w ≠ []) (ha : code.encode a = w ++ [b]) (hmax : ∀ i, (code.encode i).length ≤ (code.encode a).length) (hmissing : ∀ i, code.encode i ≠ w ++ [!b]) : totalCodeLength (code.pruneDeepest a w b hw ha hmax hmissing) + 1 = totalCodeLength code

Choose a structurally minimal no-worse competitor without assuming cost-minimizer existence.

theorem exists_minimal_totalCodeLength_competitor {α : Type*} [Fintype α] (p : α → ℝ) (original : BinaryPrefixCode α) : ∃ code : BinaryPrefixCode α, expectedCodeLength p code ≤ expectedCodeLength p original ∧ ∀ other : BinaryPrefixCode α, expectedCodeLength p other ≤ expectedCodeLength p original → totalCodeLength code ≤ totalCodeLength other

Normalize any competitor so that each deepest leaf has its sibling present.

theorem exists_competitor_with_deepest_siblings {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (original : BinaryPrefixCode α) : ∃ code : BinaryPrefixCode α, expectedCodeLength p code ≤ expectedCodeLength p original ∧ ∀ a w b, code.encode a = w ++ [b] → (∀ i, (code.encode i).length ≤ (code.encode a).length) → ∃ j, code.encode j = w ++ [!b]

Every competitor has a no-worse code containing a deepest sibling pair.

theorem exists_no_worse_deepest_sibling_pair {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (original : BinaryPrefixCode α) : ∃ code : BinaryPrefixCode α, expectedCodeLength p code ≤ expectedCodeLength p original ∧ ∃ a j w b, a ≠ j ∧ code.encode a = w ++ [b] ∧ code.encode j = w ++ [!b] ∧ ∀ i, (code.encode i).length ≤ (code.encode a).length