BanditRLProof.Algorithms.HOOTree

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

abbrev Node

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

def child (v : Node) (b : Bool) : Node

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

@[simp] theorem child_length (v : Node) (b : Bool) : (child v b).length = v.length + 1

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

theorem prefix_child (v : Node) (b : Bool) : v <+: child v b

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

def depthBound (S : Finset Node) : ℕ

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

theorem length_le_depthBound {S : Finset Node} {v : Node} (hv : v ∈ S) : v.length ≤ depthBound S

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

theorem not_mem_of_depth_lt {S : Finset Node} {v : Node} (hv : depthBound S < v.length) : v ∉ S

Unexpanded nodes have infinity; expanded nodes use the source min/max rule.

noncomputable def backward (S : Finset Node) (U : Node → WithTop ℝ) : ℕ → Node → WithTop ℝ | 0, _ => ⊤ | k+1, v => if v ∈ S then min (U v) (max (backward S U k (child v false)) (backward S U k (child v true))) else ⊤ theorem backward_not_mem (S : Finset Node) (U : Node → WithTop ℝ) (k : ℕ) (v : Node) (hv : v ∉ S) : backward S U k v = ⊤

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

theorem backward_not_mem (S : Finset Node) (U : Node → WithTop ℝ) (k : ℕ) (v : Node) (hv : v ∉ S) : backward S U k v = ⊤

Increasing already sufficient fuel has no effect on B.

theorem backward_stable_succ (S : Finset Node) (U : Node → WithTop ℝ) (k : ℕ) (v : Node) (hk : depthBound S < v.length + k) : backward S U (k+1) v = backward S U k v

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

noncomputable def bValue (S : Finset Node) (U : Node → WithTop ℝ) (v : Node) : WithTop ℝ

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

theorem bValue_not_mem (S : Finset Node) (U : Node → WithTop ℝ) (v : Node) (hv : v ∉ S) : bValue S U v = ⊤

The actual finite computation satisfies the exact recursive B equation.

theorem bValue_eq (S : Finset Node) (U : Node → WithTop ℝ) (v : Node) (hv : v ∈ S) : bValue S U v = min (U v) (max (bValue S U (child v false)) (bValue S U (child v true)))

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

noncomputable def preferred (B : Node → WithTop ℝ) (v : Node) : Bool

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

theorem preferred_max (B : Node → WithTop ℝ) (v : Node) : B (child v (preferred B v)) = max (B (child v false)) (B (child v true))

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

noncomputable def walk (S : Finset Node) (B : Node → WithTop ℝ) : ℕ → Node → Node | 0, v => v | k+1, v => if v ∈ S then walk S B k (child v (preferred B v)) else v theorem walk_not_mem (S : Finset Node) (B : Node → WithTop ℝ) (k : ℕ) (v : Node) (hk : depthBound S < v.length + k) : walk S B k v ∉ S

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

theorem walk_not_mem (S : Finset Node) (B : Node → WithTop ℝ) (k : ℕ) (v : Node) (hk : depthBound S < v.length + k) : walk S B k v ∉ S

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

theorem prefix_walk (S : Finset Node) (B : Node → WithTop ℝ) (k : ℕ) (v : Node) : v <+: walk S B k v

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

theorem walk_length_le (S : Finset Node) (B : Node → WithTop ℝ) (k : ℕ) (v : Node) : (walk S B k v).length ≤ v.length + k

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

noncomputable def select (S : Finset Node) (U : Node → WithTop ℝ) : Node

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

theorem select_not_mem (S : Finset Node) (U : Node → WithTop ℝ) : select S U ∉ S

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

theorem select_length_le (S : Finset Node) (U : Node → WithTop ℝ) : (select S U).length ≤ depthBound S + 1

The recursive optimistic value cannot decrease along the selected path.

theorem bValue_le_walk (S : Finset Node) (U : Node → WithTop ℝ) (k : ℕ) (v : Node) : bValue S U v ≤ bValue S U (walk S (bValue S U) k v)