BanditRLProof.LowerBounds.PrefixCodeSiblings

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

theorem BinaryPrefixCode.extended_prefix_parent_eq {α : Type*} (code : BinaryPrefixCode α) (a b : α) (u v : List Bool) (h : code.encode a ++ u <+: code.encode b ++ v) : a = b

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

def siblingExpandedWord {α : Type*} (code : BinaryPrefixCode (Option α)) : α ⊕ Bool → List Bool | .inl a => code.encode (some a) | .inr b => code.encode none ++ [b] theorem siblingExpandedWord_prefixFree {α : Type*} (code : BinaryPrefixCode (Option α)) {a b : α ⊕ Bool} (h : siblingExpandedWord code a <+: siblingExpandedWord code b) : a = b

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

theorem siblingExpandedWord_prefixFree {α : Type*} (code : BinaryPrefixCode (Option α)) {a b : α ⊕ Bool} (h : siblingExpandedWord code a <+: siblingExpandedWord code b) : a = b

Split a designated merged leaf into two siblings.

def BinaryPrefixCode.expandSibling {α : Type*} (code : BinaryPrefixCode (Option α)) : BinaryPrefixCode (α ⊕ Bool) where

Exact cost recurrence of splitting a merged symbol.

theorem expectedCodeLength_expandSibling {α : Type*} [Fintype α] (code : BinaryPrefixCode (Option α)) (p : α → ℝ) (q r : ℝ) : expectedCodeLength (Sum.elim p (fun b => if b then r else q)) code.expandSibling = expectedCodeLength (fun a => a.elim (q + r) p) code + q + r

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

theorem sibling_parent_not_prefix_other {α : Type*} (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (hs : ∀ b, code.encode (.inr b) = w ++ [b]) (a : α) : ¬ w <+: code.encode (.inl a)

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

def siblingContractedWord {α : Type*} (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) : Option α → List Bool | none => w | some a => code.encode (.inl a) theorem siblingContractedWord_prefixFree {α : Type*} (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (hs : ∀ b, code.encode (.inr b) = w ++ [b]) {a b : Option α} (h : siblingContractedWord code w a <+: siblingContractedWord code w b) : a = b

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

theorem siblingContractedWord_prefixFree {α : Type*} (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (hs : ∀ b, code.encode (.inr b) = w ++ [b]) {a b : Option α} (h : siblingContractedWord code w a <+: siblingContractedWord code w b) : a = b

Merge two actual sibling leaves whose parent is nonempty.

def BinaryPrefixCode.contractSibling {α : Type*} (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (hw : w ≠ []) (hs : ∀ b, code.encode (.inr b) = w ++ [b]) : BinaryPrefixCode (Option α) where

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

theorem expectedCodeLength_contractSibling {α : Type*} [Fintype α] (code : BinaryPrefixCode (α ⊕ Bool)) (w : List Bool) (hw : w ≠ []) (hs : ∀ b, code.encode (.inr b) = w ++ [b]) (p : α → ℝ) (q r : ℝ) : expectedCodeLength (fun a => a.elim (q + r) p) (code.contractSibling w hw hs) + q + r = expectedCodeLength (Sum.elim p (fun b => if b then r else q)) code

The two-symbol root code, avoiding an invalid empty parent codeword.

def binaryRootPrefixCode : BinaryPrefixCode Bool where

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

theorem binaryRootPrefixCode_optimal (p : Bool → ℝ) (hp : ∀ b, 0 ≤ p b) (hs : ∑ b, p b = 1) : IsOptimalPrefixCode p binaryRootPrefixCode