Lean module · Foundations
BanditRLProof.Algorithms.HOOPathComparison
Actual HOO search-path comparison with a supremum-preserving branch.
Module map
Imports
BanditRLProof.HOOOptimalBranch, BanditRLProof.Algorithms.HOOPrefix
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.branch_root_optimistic
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.branch_root_optimisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.branch_root_optimistic {X : Type*} (C : Covering X) (f : X → ℝ) (S : Finset Node) (U : Node → WithTop ℝ) (best : ℝ) (k : ℕ) (hk : C.optimalPath f k ∉ S) (hpre : ∀ j < k, C.optimalPath f j ∈ S) (hU : ∀ j < k, (best : WithTop ℝ) ≤ U (C.optimalPath f j)) : (best : WithTop ℝ) ≤ bValue S U []
theorem
BanditRLProof.HOO.Covering.selected_underestimate_implies_branch_underestimate
Compiled
If an expanded region lies on the actual selected path but has U below `best`, some node of the comparison branch has U below `best`. The branch need only be inspected through the finite tree's maximum depth.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.selected_underestimate_implies_branch_underestimateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.selected_underestimate_implies_branch_underestimate {X : Type*} (C : Covering X) (f : X → ℝ) (S : Finset Node) (U : Node → WithTop ℝ) (best : ℝ) (v : Node) (hv : v ∈ S) (hpath : v <+: select S U) (hU : U v < (best : WithTop ℝ)) : ∃ j ≤ depthBound S, U (C.optimalPath f j) < (best : WithTop ℝ)
theorem
BanditRLProof.HOO.Covering.history_selected_underestimate
Compiled
The same comparison stated directly on the generated chronological state.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.Covering.history_selected_underestimateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.history_selected_underestimate {X : Type*} (C : Covering X) (f : X → ℝ) (ν ρ best : ℝ) (Y : ℕ → ℝ) (n : ℕ) (v : Node) (hv : v ∈ expanded (history ν ρ Y n)) (hpath : v <+: action ν ρ Y n) (hu : upper ν ρ (history ν ρ Y n) v < (best : WithTop ℝ)) : ∃ j ≤ n, upper ν ρ (history ν ρ Y n) (C.optimalPath f j) < (best : WithTop ℝ)