Lean module · Foundations
BanditRLProof.LowerBounds.PrefixCodeGreedy
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.PrefixCodePruning
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.expectedCodeLength_swap_le_allow_eq
Compiled
The exchange bound also permits an already correctly placed label.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.expectedCodeLength_swap_le_allow_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expectedCodeLength_swap_le_allow_eq {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a b : α) (hp : p a ≤ p b) (hl : (code.encode a).length ≤ (code.encode b).length) : expectedCodeLength p (code.relabel (Equiv.swap a b)) ≤ expectedCodeLength p code
theorem
BanditRLProof.LowerBounds.exists_no_worse_least_weight_siblings
Compiled
Huffman's greedy choice: any competitor can place two specified least weights at deepest sibling leaves without increasing expected length. Ties and zero weights are permitted, and no existence of an optimal code is assumed.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_no_worse_least_weight_siblingsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_no_worse_least_weight_siblings {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (original : BinaryPrefixCode α) (a b : α) (hab : a ≠ b) (ha : ∀ i, p a ≤ p i) (hb : ∀ i, i ≠ a → p b ≤ p i) : ∃ code : BinaryPrefixCode α, expectedCodeLength p code ≤ expectedCodeLength p original ∧ ∃ w bit, code.encode a = w ++ [bit] ∧ code.encode b = w ++ [!bit] ∧ ∀ i, (code.encode i).length ≤ (code.encode a).length