BanditRLProof.LowerBounds.ArithmeticBlockCoding

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

def sourceBlockList {α : Type*} : (n : ℕ) → SourceBlock α n → List α | 0, _ => [] | n + 1, x => x.1 :: sourceBlockList n x.2 theorem sourceBlockList_length {α : Type*} (n : ℕ) (x : SourceBlock α n) : (sourceBlockList n x).length = n

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

theorem sourceBlockList_length {α : Type*} (n : ℕ) (x : SourceBlock α n) : (sourceBlockList n x).length = n

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

theorem sourceBlockList_injective {α : Type*} (n : ℕ) : Function.Injective (sourceBlockList (α := α) n)

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

theorem sourceBlockList_mass {α : Type*} (p : α → ℝ) (n : ℕ) (x : SourceBlock α n) : ((sourceBlockList n x).map p).prod = sourceBlockMass p n x

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

theorem exists_arithmeticBlockSupport {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) : ∃ positive : BinaryPrefixCode {x : SourceBlock.{0,0} (Fin k) n // 0 < sourceBlockMass p n x}, (∀ x, (positive.encode x).length = arithmeticLength (sourceBlockMass p n x.val)) ∧ (∀ x, (arithmeticInterval p (sourceBlockList n x.val)).1 ≤ dyadicAddressLower (positive.encode x) ∧ dyadicAddressUpper (positive.encode x) < (arithmeticInterval p (sourceBlockList n x.val)).2) ∧ expectedCodeLength (sourceBlockMass p n) (positive.extendZeroMass (sourceBlockMass p n) (huffmanCode (sourceBlockMass p n) (sourceBlockMass_nonneg p hp n))) ≤ n * discreteEntropyBaseTwo Finset.univ p + 3

The named arithmetic block code: interval addresses on positive blocks, with the one-bit tagged fallback on zero-mass blocks.

noncomputable def arithmeticBlockCode {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) : BinaryPrefixCode (SourceBlock.{0,0} (Fin k) n)

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

theorem arithmeticBlockCode_expected_length_le {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) : expectedCodeLength (sourceBlockMass p n) (arithmeticBlockCode p hp hs n) ≤ n * discreteEntropyBaseTwo Finset.univ p + 3

Removing the support tag from a positive block yields an address inside its actual arithmetic interval. This property belongs to the named code, not merely to an unrelated witness with the same length.

theorem arithmeticBlockCode_payload_interval {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) (x : SourceBlock.{0,0} (Fin k) n) (hx : 0 < sourceBlockMass p n x) : (arithmeticInterval p (sourceBlockList n x)).1 ≤ dyadicAddressLower ((arithmeticBlockCode p hp hs n).encode x).tail ∧ dyadicAddressUpper ((arithmeticBlockCode p hp hs n).encode x).tail < (arithmeticInterval p (sourceBlockList n x)).2

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

theorem arithmeticBlockCode_rate_sandwich {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) (hn : 0 < n) : discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength (sourceBlockMass p n) (arithmeticBlockCode p hp hs n) / n ∧ expectedCodeLength (sourceBlockMass p n) (arithmeticBlockCode p hp hs n) / n ≤ discreteEntropyBaseTwo Finset.univ p + 3 / n

The constructed arithmetic code's expected bits per symbol tend to entropy, including sources with zero-probability symbols.

theorem arithmeticBlockCode_rate_tendsto_entropy {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : Filter.Tendsto (fun n : ℕ => expectedCodeLength (sourceBlockMass p (n + 1)) (arithmeticBlockCode p hp hs (n + 1)) / (n + 1)) Filter.atTop (nhds (discreteEntropyBaseTwo Finset.univ p))