BanditRLProof.HOOModel

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

structure Covering (X : Type*) where

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

theorem Covering.child_subset {X : Type*} (C : Covering X) (v : Node) (b : Bool) : C.region (child v b) ⊆ C.region v

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

theorem Covering.append_subset {X : Type*} (C : Covering X) (v u : Node) : C.region (v ++ u) ⊆ C.region v

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

theorem Covering.descendant_subset {X : Type*} (C : Covering X) {v w : Node} (h : v <+: w) : C.region w ⊆ C.region v

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

noncomputable def Covering.representative {X : Type*} (C : Covering X) (v : Node) : X

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

theorem Covering.representative_mem {X : Type*} (C : Covering X) (v : Node) : C.representative v ∈ C.region v

A1, stated with pointwise diameter bounds equivalent to the source bound. Inner balls need not be metric balls: asymmetry and lack of triangle inequality are retained.

structure RegularCovering (X : Type*) [MeasurableSpace X] extends Covering X where

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

theorem RegularCovering.region_near_optimal {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best c : ℝ) (v : Node) (hw : WeaklyLipschitz f C.ell best) (hgap : best - regionSup f (C.region v) ≤ c*(C.nu1*C.rho^v.length)) (y : X) (hy : y ∈ C.region v) : best - f y ≤ max (2*c) (c+1)*(C.nu1*C.rho^v.length)

Fixed representatives are allowed by source Algorithm 1. Their countable domain makes the arm-to-law map measurable without requiring a continuous selector on the entire arm space.

noncomputable def Covering.nodeLaw {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) : Kernel Node ℝ

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

noncomputable def Covering.arm {X : Type*} (C : Covering X) (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : X

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

theorem Covering.arm_mem {X : Type*} (C : Covering X) (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : C.arm ν ρ Y n ∈ C.region (action ν ρ Y n)

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

theorem Covering.measurable_arm {X : Type*} [MeasurableSpace X] (C : Covering X) (ν ρ : ℝ) (n : ℕ) : Measurable (fun Y => C.arm ν ρ Y n)

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

theorem Covering.stepKernel_actual_arm {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : stepKernel ν ρ (C.nodeLaw law) n (Preorder.frestrictLe n Y) = law (C.arm ν ρ Y (n+1))