Lean module · Foundations
BanditRLProof.HOOOptimalBranch
A deterministic branch preserving regional suprema. No maximizer or attainment of any regional supremum is assumed.
Module map
Imports
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HOO.Covering.regionSup_children
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.regionSup_childrenReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.regionSup_children {X : Type*} (C : Covering X) (f : X → ℝ) (best : ℝ) (hf : ∀ x, f x ≤ best) (v : Node) : regionSup f (C.region v) = max (regionSup f (C.region (child v false))) (regionSup f (C.region (child v true)))
def
BanditRLProof.HOO.Covering.optimalChild
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalChildReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def Covering.optimalChild {X : Type*} (C : Covering X) (f : X → ℝ) (v : Node) : Bool
theorem
BanditRLProof.HOO.Covering.optimalChild_sup
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalChild_supReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.optimalChild_sup {X : Type*} (C : Covering X) (f : X → ℝ) (best : ℝ) (hf : ∀ x, f x ≤ best) (v : Node) : regionSup f (C.region (child v (C.optimalChild f v))) = regionSup f (C.region v)
def
BanditRLProof.HOO.Covering.optimalPath
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalPathReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def Covering.optimalPath {X : Type*} (C : Covering X) (f : X → ℝ) : ℕ → Node | 0 => [] | n+1 => child (C.optimalPath f n) (C.optimalChild f (C.optimalPath f n)) @[simp] theorem Covering.optimalPath_length {X : Type*} (C : Covering X) (f : X → ℝ) (n : ℕ) : (C.optimalPath f n).length = n
theorem
BanditRLProof.HOO.Covering.optimalPath_length
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalPath_lengthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem Covering.optimalPath_length {X : Type*} (C : Covering X) (f : X → ℝ) (n : ℕ) : (C.optimalPath f n).length = n
theorem
BanditRLProof.HOO.Covering.optimalPath_sup
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalPath_supReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.optimalPath_sup {X : Type*} (C : Covering X) (f : X → ℝ) (best : ℝ) (hf : ∀ x, f x ≤ best) (n : ℕ) : regionSup f (C.region (C.optimalPath f n)) = regionSup f Set.univ
theorem
BanditRLProof.HOO.Covering.optimalPath_prefix
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.optimalPath_prefixReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.optimalPath_prefix {X : Type*} (C : Covering X) (f : X → ℝ) {i j : ℕ} (hij : i ≤ j) : C.optimalPath f i <+: C.optimalPath f j
theorem
BanditRLProof.HOO.Covering.exists_first_unexpanded
Compiled
Every finite expanded tree has a first missing node on this infinite branch, bounded by its maximum depth plus one.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.exists_first_unexpandedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.exists_first_unexpanded {X : Type*} (C : Covering X) (f : X → ℝ) (S : Finset Node) : ∃ k ≤ depthBound S + 1, C.optimalPath f k ∉ S ∧ ∀ j < k, C.optimalPath f j ∈ S