BanditRLProof.HOOPartition

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

@[simp] theorem RegularCovering.mem_nearOptimalNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (v : Node) (h : ℕ) : v ∈ C.nearOptimalNodes f best h ↔ v.length=h ∧ best-regionSup f (C.region v) ≤ 2*(C.nu1*C.rho^h)

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

theorem RegularCovering.root_nearOptimal {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hbest : regionSup f Set.univ = best) : [] ∈ C.nearOptimalNodes f best 0

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

theorem RegularCovering.nearOptimal_prefix {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hf : ∀x, f x ≤ best) {v w : Node} (hp : v <+: w) (hw : w ∈ C.nearOptimalNodes f best w.length) : v ∈ C.nearOptimalNodes f best v.length

Indexed by the parent's depth: this is source J_(h+1).

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

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

theorem RegularCovering.mem_boundaryNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (h : ℕ) (v : Node) : v ∈ C.boundaryNodes f best h ↔ (∃ p ∈ C.nearOptimalNodes f best h, ∃ b, child p b=v) ∧ v ∉ C.nearOptimalNodes f best (h+1)

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

theorem RegularCovering.boundaryNodes_card_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (h : ℕ) : (C.boundaryNodes f best h).card ≤ 2*(C.nearOptimalNodes f best h).card

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

theorem RegularCovering.boundaryNodes_poor {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) {h : ℕ} {v : Node} (hv : v ∈ C.boundaryNodes f best h) : v.length=h+1 ∧ 2*(C.nu1*C.rho^(h+1)) < best-regionSup f (C.region v)

Any word either lies below a good depth-H prefix, is itself a shallow near-optimal word, or lies below a first bad child of a near-optimal parent.

theorem RegularCovering.node_partition_cover {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hbest : regionSup f Set.univ=best) (H : ℕ) (v : Node) : (∃ p ∈ C.nearOptimalNodes f best H, p <+: v) ∨ (v.length<H ∧ v ∈ C.nearOptimalNodes f best v.length) ∨ (∃ h < H, ∃ p ∈ C.boundaryNodes f best h, p <+: v)

The deep-good and shallow-good regret bounds use Lemma 3 on the actual representative in a descendant region.

theorem RegularCovering.descendant_nearOptimal_gap {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) {p v : Node} {h : ℕ} (hp : p ∈ C.nearOptimalNodes f best h) (hv : p <+: v) : best-f (C.toCovering.representative v) ≤ 4*(C.nu1*C.rho^h)

Poor subtrees inherit their parent's gap bound, not the poor child's gap.

theorem RegularCovering.descendant_boundary_gap {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) {p v : Node} {h : ℕ} (hp : p ∈ C.boundaryNodes f best h) (hv : p <+: v) : best-f (C.toCovering.representative v) ≤ 4*(C.nu1*C.rho^h)

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

private theorem prefix_of_prefixes_length {p q v : Node} (hp : p <+: v) (hq : q <+: v) (hl : p.length≤q.length) : p <+: q

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

def RegularCovering.deepGoodNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (H : ℕ) : Set Node

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

def RegularCovering.shallowGoodNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (H : ℕ) : Set Node

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

def RegularCovering.badSubtreeNodes {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (H : ℕ) : Set Node

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

theorem RegularCovering.deep_shallow_disjoint {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (H : ℕ) : Disjoint (C.deepGoodNodes f best H) (C.shallowGoodNodes f best H)

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

theorem RegularCovering.deep_bad_disjoint {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hf : ∀x, f x≤best) (H : ℕ) : Disjoint (C.deepGoodNodes f best H) (C.badSubtreeNodes f best H)

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

theorem RegularCovering.shallow_bad_disjoint {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hf : ∀x, f x≤best) (H : ℕ) : Disjoint (C.shallowGoodNodes f best H) (C.badSubtreeNodes f best H)

Exact three-part identity for the actual HOO action trace, before any inequality or expectation. Cover and disjointness are derived above.

theorem RegularCovering.actual_regret_partition {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hf : ∀x, f x≤best) (hbest : regionSup f Set.univ=best) (H N : ℕ) (Y : ℕ → ℝ) : (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) = (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.deepGoodNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0) + (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.shallowGoodNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0) + (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.badSubtreeNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0)