BanditRLProof.HOOPacking

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

structure ContainedBallPacking {X I : Type*} (ell : X → X → ℝ) (A : Set X) (ε : ℝ) (centers : I → X) : Prop where

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

def packingSizes {X : Type*} (ell : X → X → ℝ) (A : Set X) (ε : ℝ) : Set ℕ

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

theorem zero_mem_packingSizes {X : Type*} (ell : X → X → ℝ) (A : Set X) (ε : ℝ) : 0 ∈ packingSizes ell A ε

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

theorem RegularCovering.packingSizes_bddAbove {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (A : Set X) (ε : ℝ) (hε : 0 < ε) : BddAbove (packingSizes C.ell A ε)

Natural-valued source packing number on an A1 space. All semantic theorems below require positive radius, where finiteness is proved.

noncomputable def RegularCovering.packingNumber {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (A : Set X) (ε : ℝ) : ℕ

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

theorem RegularCovering.packingNumber_attained {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (A : Set X) (ε : ℝ) (hε : 0 < ε) : ∃ centers : Fin (C.packingNumber A ε) → X, ContainedBallPacking C.ell A ε centers

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

theorem RegularCovering.packingNumber_mono {X : Type*} [MeasurableSpace X] (C : RegularCovering X) {A B : Set X} (hAB : A ⊆ B) (ε : ℝ) (hε : 0 < ε) : C.packingNumber A ε ≤ C.packingNumber B ε

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

theorem RegularCovering.containedPacking_card_le {X I : Type*} [MeasurableSpace X] [Fintype I] (C : RegularCovering X) (A : Set X) (ε : ℝ) (hε : 0 < ε) (centers : I → X) (hc : ContainedBallPacking C.ell A ε centers) : Fintype.card I ≤ C.packingNumber A ε

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

noncomputable def RegularCovering.nearOptimalNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (h : ℕ) : Finset Node

Source Theorem 6, second-step packing producer for the actual near-optimal nodes. It constructs contained balls via A1 and Lemma 3 with c=2.

theorem RegularCovering.nearOptimalNodes_card_le_packing {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) (h : ℕ) : (C.nearOptimalNodes f best h).card ≤ C.packingNumber {y | best-f y ≤ 4*(C.nu1*C.rho^h)} (C.nu2*C.rho^h)

Larger-radius contained packings inject into an ambient smaller-radius packing by shrinking every ball, without symmetry or a triangle inequality.

theorem RegularCovering.packingNumber_le_ambient {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (A : Set X) {δ ε : ℝ} (hδ : 0<δ) (hδε : δ≤ε) : C.packingNumber A ε ≤ C.packingNumber Set.univ δ