BanditRLProof.LowerBounds.ArithmeticZeroExtension

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

noncomputable def supportTaggedWord {α : Type*} (p : α → ℝ) (positive : BinaryPrefixCode {a // 0 < p a}) (fallback : BinaryPrefixCode α) (a : α) : List Bool

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

theorem supportTaggedWord_prefixFree {α : Type*} (p : α → ℝ) (positive : BinaryPrefixCode {a // 0 < p a}) (fallback : BinaryPrefixCode α) {a b : α} (h : supportTaggedWord p positive fallback a <+: supportTaggedWord p positive fallback b) : a = b

Extend an arithmetic support code to all symbols, with a one-bit escape tag.

noncomputable def BinaryPrefixCode.extendZeroMass {α : Type*} (p : α → ℝ) (positive : BinaryPrefixCode {a // 0 < p a}) (fallback : BinaryPrefixCode α) : BinaryPrefixCode α where

Zero-mass fallback words cost nothing in expectation. The extra support tag adds only one bit to a support code with information-plus-two length bound.

theorem expectedCodeLength_extendZeroMass_le {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ a, 0 ≤ p a) (hs : ∑ a, p a = 1) (positive : BinaryPrefixCode {a // 0 < p a}) (fallback : BinaryPrefixCode α) (hpos : ∀ a (ha : 0 < p a), ((positive.encode ⟨a, ha⟩).length : ℝ) ≤ Real.log (p a)⁻¹ / Real.log 2 + 2) : expectedCodeLength p (positive.extendZeroMass p fallback) ≤ discreteEntropyBaseTwo Finset.univ p + 3

Arithmetic coding on the positive support, extended to every message. Only the zero-mass escape branch uses the supplied total Huffman fallback.

theorem exists_zeroSafe_arithmeticCode {α : Type*} [Fintype α] {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (message : α → List (Fin k)) (hinj : Function.Injective message) (hlen : ∀ a b, (message a).length = (message b).length) (q : α → ℝ) (hq : ∀ a, 0 ≤ q a) (hqs : ∑ a, q a = 1) (hmass : ∀ a, ((message a).map p).prod = q a) : ∃ positive : BinaryPrefixCode {a // 0 < q a}, (∀ a, (positive.encode a).length = arithmeticLength (q a.val)) ∧ (∀ a, (arithmeticInterval p (message a.val)).1 ≤ dyadicAddressLower (positive.encode a) ∧ dyadicAddressUpper (positive.encode a) < (arithmeticInterval p (message a.val)).2) ∧ expectedCodeLength q (positive.extendZeroMass q (huffmanCode q hq)) ≤ discreteEntropyBaseTwo Finset.univ q + 3