BanditRLProof.LowerBounds.PrefixCodeExchange

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

def BinaryPrefixCode.relabel {α β : Type*} (code : BinaryPrefixCode α) (e : β ≃ α) : BinaryPrefixCode β where

Full optimality against every code, not merely against a chosen candidate family.

def IsOptimalPrefixCode {α : Type*} [Fintype α] (p : α → ℝ) (code : BinaryPrefixCode α) : Prop

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

theorem expectedCodeLength_swap {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a b : α) (hab : a ≠ b) : expectedCodeLength p (code.relabel (Equiv.swap a b)) = expectedCodeLength p code + (p a - p b) * ((code.encode b).length - (code.encode a).length : ℝ)

Assigning a shorter word to a higher-probability symbol cannot increase cost.

theorem expectedCodeLength_swap_le {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (code : BinaryPrefixCode α) (a b : α) (hab : 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

An optimal code orders lengths opposite to strictly ordered probabilities.

theorem IsOptimalPrefixCode.length_antitone {α : Type*} [Fintype α] [DecidableEq α] {p : α → ℝ} {code : BinaryPrefixCode α} (hopt : IsOptimalPrefixCode p code) (a b : α) (hp : p a < p b) : (code.encode b).length ≤ (code.encode a).length

Any global minimizer inherits the entropy sandwich; this does not assert existence.

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

The local nonempty-codeword convention forces at least one expected bit.

theorem one_le_expectedCodeLength {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (code : BinaryPrefixCode α) : 1 ≤ expectedCodeLength p code

The singleton alphabet's nonempty one-bit code.

def singletonPrefixCode (α : Type*) [Subsingleton α] : BinaryPrefixCode α where

The singleton base case has a genuine global optimum under the local convention.

theorem singletonPrefixCode_optimal {α : Type*} [Fintype α] [Subsingleton α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : IsOptimalPrefixCode p (singletonPrefixCode α)