BanditRLProof.HOOCantorModel

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

abbrev Arm

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

def center (v : Node) : Arm

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

def region (v : Node) : Set Arm

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

noncomputable def ell (x y : Arm) : ℝ

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

theorem center_child_of_lt (v : Node) (b : Bool) (i : ℕ) (hi : i < v.length) : center (child v b) i = center v i

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

@[simp] theorem center_child_last (v : Node) (b : Bool) : center (child v b) v.length = b

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

theorem mem_child_iff (v : Node) (b : Bool) (x : Arm) : x ∈ region (child v b) ↔ x ∈ region v ∧ x v.length = b

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

theorem region_children (v : Node) : region v = region (child v false) ∪ region (child v true)

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

theorem region_measurable (v : Node) : MeasurableSet (region v)

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

theorem region_diameter (v : Node) (x : Arm) (hx : x ∈ region v) (y : Arm) (hy : y ∈ region v) : ell x y ≤ (1/2:ℝ)^v.length

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

theorem ball_subset_region (v : Node) : {y : Arm | ell (center v) y < (1/2:ℝ)^v.length} ⊆ region v

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

theorem region_disjoint {v w : Node} (hl : v.length=w.length) (hne : v≠w) : Disjoint (region v) (region w)

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

noncomputable def covering : RegularCovering Arm where

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

noncomputable def mean (x : Arm) : ℝ

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

theorem mean_le_best (x : Arm) : mean x ≤ 1/2

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

theorem first_coordinate_distance (x y : Arm) (h : x 0 ≠ y 0) : ell x y = 1

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

theorem weaklyLipschitz : WeaklyLipschitz mean ell (1/2)

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

noncomputable def bitReward (b : Bool) : Measure ℝ

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

noncomputable def bitKernel : Kernel Bool ℝ

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

noncomputable def law : Kernel Arm ℝ

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

theorem law_bounded (x : Arm) : ∀ᵐ y ∂law x, y ∈ Set.Icc (0 : ℝ) 1

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

theorem law_zero_mass (x : Arm) : law x {0} = (1/2 : ENNReal)

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

theorem law_not_dirac (x : Arm) (r : ℝ) : law x ≠ Measure.dirac r

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

theorem law_mean (x : Arm) : (∫ y, y ∂law x) = mean x

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

theorem global_sup : regionSup mean Set.univ = 1/2

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

def poorNode : Node

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

theorem poor_region_mean (x : Arm) (hx : x ∈ region poorNode) : mean x = 1/4

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

theorem poor_sup : regionSup mean (region poorNode) = 1/4

A concrete nontrivial poor region in the infinite-arm model consumes the complete algorithm-to-expected-visits chain.

theorem expected_poor_visits (N : ℕ) : (∫ Y, (visits (history 1 (1/2) Y N) poorNode : ℝ) ∂trajectory 1 (1/2) (covering.toCovering.nodeLaw law)) ≤ 512 * Real.log (max (N:ℝ) 2) + 4