BanditRLProof.LowerBounds.ArithmeticIntervals

Left endpoint of a symbol's arithmetic-coding partition cell.

def arithmeticOffset {k : ℕ} (p : Fin k → ℝ) (a : Fin k) : ℝ

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

theorem arithmeticOffset_nonneg {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (a : Fin k) : 0 ≤ arithmeticOffset p a

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

theorem arithmeticOffset_add_le_one {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (a : Fin k) : arithmeticOffset p a + p a ≤ 1

Successive affine subdivisions for an arithmetic-coded word.

def arithmeticInterval {k : ℕ} (p : Fin k → ℝ) : List (Fin k) → ℝ × ℝ | [] => (0, 1) | a :: w => (arithmeticOffset p a + p a * (arithmeticInterval p w).1, arithmeticOffset p a + p a * (arithmeticInterval p w).2) theorem arithmeticInterval_width {k : ℕ} (p : Fin k → ℝ) (w : List (Fin k)) : (arithmeticInterval p w).2 - (arithmeticInterval p w).1 = (w.map p).prod

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

theorem arithmeticInterval_width {k : ℕ} (p : Fin k → ℝ) (w : List (Fin k)) : (arithmeticInterval p w).2 - (arithmeticInterval p w).1 = (w.map p).prod

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

theorem arithmeticInterval_bounds {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (w : List (Fin k)) : 0 ≤ (arithmeticInterval p w).1 ∧ (arithmeticInterval p w).1 ≤ (arithmeticInterval p w).2 ∧ (arithmeticInterval p w).2 ≤ 1

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

theorem arithmeticOffset_separated {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (a b : Fin k) (hab : a < b) : arithmeticOffset p a + p a ≤ arithmeticOffset p b

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

theorem arithmeticInterval_head_separated {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (a b : Fin k) (u v : List (Fin k)) (hab : a < b) : (arithmeticInterval p (a :: u)).2 ≤ (arithmeticInterval p (b :: v)).1

Different equal-length messages occupy cells with disjoint interiors.

theorem arithmeticInterval_separated {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (u v : List (Fin k)) (hlen : u.length = v.length) (hne : u ≠ v) : (arithmeticInterval p u).2 ≤ (arithmeticInterval p v).1 ∨ (arithmeticInterval p v).2 ≤ (arithmeticInterval p u).1

Any point strictly inside a message cell identifies that message uniquely among messages of the same length.

theorem arithmeticInterval_interior_unique {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (u v : List (Fin k)) (hlen : u.length = v.length) (x : ℝ) (hu : (arithmeticInterval p u).1 < x ∧ x < (arithmeticInterval p u).2) (hv : (arithmeticInterval p v).1 < x ∧ x < (arithmeticInterval p v).2) : u = v

A positive grid cell fits in any nonnegative interval at least twice as wide. Mathlib-candidate scalar rounding leaf for arithmetic-code dyadic selection.

theorem exists_grid_cell_inside (L U δ : ℝ) (hL : 0 ≤ L) (hδ : 0 < δ) (hwidth : 2 * δ ≤ U - L) : ∃ m : ℕ, L ≤ (m : ℝ) * δ ∧ ((m : ℝ) + 1) * δ < U