BanditRLProof.HOODimension

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

noncomputable def RegularCovering.nearOptimalPacking {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c ε : ℝ) : ℕ

The normalized extended logarithm. At zero packing the value is minus infinity; this does not invoke the totalized real logarithm at zero.

noncomputable def packingExponent (N : ℕ) (ε : ℝ) : EReal

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

@[simp] theorem packingExponent_zero (ε : ℝ) : packingExponent 0 ε = ⊥

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

theorem packingExponent_positive {N : ℕ} (hN : 0<N) (ε : ℝ) : packingExponent N ε = (Real.log (N:ℝ) / Real.log (1/ε) : ℝ)

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

noncomputable def RegularCovering.nearOptimalityDimension {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c : ℝ) : EReal

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

theorem RegularCovering.nearOptimalityDimension_nonneg {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c : ℝ) : 0 ≤ C.nearOptimalityDimension f best c

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

theorem packing_le_rpow_of_exponent_lt {N : ℕ} {ε d : ℝ} (hε : 0<ε) (hε1 : ε<1) (h : packingExponent N ε < (d:EReal)) : (N:ℝ) ≤ ε^(-d)

Strictly exceeding the actual limsup dimension produces a fine-scale packing bound; no power-law packing premise is assumed.

theorem RegularCovering.eventually_nearOptimalPacking_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c d : ℝ) (hd : C.nearOptimalityDimension f best c < (d:EReal)) : ∀ᶠ ε in 𝓝[>] (0:ℝ), (C.nearOptimalPacking f best c ε : ℝ) ≤ ε^(-d)

Source Theorem 6's uniform constant, including all coarse scales up to R. The fine-scale bound comes from Definition 5, the coarse bound from A1.

theorem RegularCovering.uniform_nearOptimalPacking_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c d R : ℝ) (hR : 0<R) (hd : C.nearOptimalityDimension f best c < (d:EReal)) : ∃ K : ℝ, 0<K ∧ ∀ ε : ℝ, 0<ε → ε≤R → (C.nearOptimalPacking f best c ε : ℝ) ≤ K * ε^(-d)

Actual near-optimal tree levels inherit the power bound at the exact source parameter c=4*nu1/nu2. The constant is independent of depth.

theorem RegularCovering.nearOptimalNodes_power_bound {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best d : ℝ) (hw : WeaklyLipschitz f C.ell best) (hd : C.nearOptimalityDimension f best (4*C.nu1/C.nu2) < (d:EReal)) : ∃ K : ℝ, 0<K ∧ ∀ h : ℕ, ((C.nearOptimalNodes f best h).card : ℝ) ≤ K * (C.nu2*C.rho^h)^(-d)