BanditRLProof.LowerBounds.ArithmeticPrefixCode

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

theorem arithmeticAddress_prefix_forces_eq {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (u v : List (Fin k)) (hlen : u.length = v.length) (cu cv : List Bool) (huL : (arithmeticInterval p u).1 ≤ dyadicAddressLower cu) (huU : dyadicAddressUpper cu < (arithmeticInterval p u).2) (hvL : (arithmeticInterval p v).1 ≤ dyadicAddressLower cv) (hvU : dyadicAddressUpper cv < (arithmeticInterval p v).2) (hprefix : cu <+: cv) : u = v

Assemble arithmetic-cell addresses into a genuine prefix code, preserving the supplied bit lengths. The width budgets are discharged by later allocation.

theorem exists_arithmeticPrefixCode {α : Type*} {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) (bits : α → ℕ) (hbudget : ∀ a, 2 * (1 / (2 : ℝ) ^ bits a) ≤ (arithmeticInterval p (message a)).2 - (arithmeticInterval p (message a)).1) : ∃ code : BinaryPrefixCode α, (∀ a, (code.encode a).length = bits a) ∧ ∀ a, (arithmeticInterval p (message a)).1 ≤ dyadicAddressLower (code.encode a) ∧ dyadicAddressUpper (code.encode a) < (arithmeticInterval p (message a)).2

One extra bit beyond strict Shannon length fits a dyadic cell inside the arithmetic interval, rather than merely meeting a Kraft budget.

noncomputable def arithmeticLength (mass : ℝ) : ℕ

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

theorem arithmeticLength_width_budget {mass : ℝ} (hm : 0 < mass) : 2 * (1 / (2 : ℝ) ^ arithmeticLength mass) < mass

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

theorem arithmeticLength_le_information_add_two {mass : ℝ} (hm : 0 < mass) (hm1 : mass ≤ 1) : (arithmeticLength mass : ℝ) ≤ Real.log mass⁻¹ / Real.log 2 + 2