Lean module · Foundations
BanditRLProof.LowerBounds.HuffmanStep
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.PrefixCodeGreedy
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.exists_oriented_sibling_code
Compiled
Orient an actual pair of sibling leaves without changing its cost.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_oriented_sibling_codeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_oriented_sibling_code {α : Type*} [Fintype α] [DecidableEq α] (p : α ⊕ Bool → ℝ) (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (bit : Bool) (hf : code.encode (.inr false) = w ++ [bit]) (ht : code.encode (.inr true) = w ++ [!bit]) : ∃ other : BinaryPrefixCode (α ⊕ Bool), expectedCodeLength p other = expectedCodeLength p code ∧ ∀ b, other.encode (.inr b) = w ++ [b]
theorem
BanditRLProof.LowerBounds.IsOptimalPrefixCode.expand_least_weights
Compiled
The Huffman induction step: expanding an optimal merged code is globally optimal when the split symbols are the two least weights.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.IsOptimalPrefixCode.expand_least_weightsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem IsOptimalPrefixCode.expand_least_weights {α : Type*} [Fintype α] [DecidableEq α] [Nonempty α] (p : α → ℝ) (q r : ℝ) (hp : ∀ i, 0 ≤ p i) (hq : 0 ≤ q) (hqr : q ≤ r) (hr : ∀ i, r ≤ p i) (code : BinaryPrefixCode (Option α)) (hopt : IsOptimalPrefixCode (fun a => a.elim (q + r) p) code) : IsOptimalPrefixCode (Sum.elim p (fun b => if b then r else q)) code.expandSibling