Lean module · Foundations
BanditRLProof.Algorithms.HOOPrefix
Actual selected-path and prefix-closure producers for source Lemma 14.
Module map
Imports
BanditRLProof.Algorithms.HOOHistory
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.proper_prefix_walk_mem
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.proper_prefix_walk_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem proper_prefix_walk_mem (S : Finset Node) (B : Node → WithTop ℝ) (k : ℕ) (v w : Node) (hvw : v <+: w) (hw : w <+: walk S B k v) (hne : w ≠ walk S B k v) : w ∈ S
theorem
BanditRLProof.HOO.proper_prefix_select_mem
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.proper_prefix_select_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem proper_prefix_select_mem (S : Finset Node) (U : Node → WithTop ℝ) (w : Node) (hw : w <+: select S U) (hne : w ≠ select S U) : w ∈ S
theorem
BanditRLProof.HOO.expanded_history_prefix_closed
Compiled
The generated tree is prefix closed; it is not assumed to be a valid tree.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.expanded_history_prefix_closedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expanded_history_prefix_closed (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) (w v : Node) (hw : w ∈ expanded (history ν ρ Y n)) (hv : v <+: w) : v ∈ expanded (history ν ρ Y n)
theorem
BanditRLProof.HOO.bValue_le_upper
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.bValue_le_upperReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bValue_le_upper (S : Finset Node) (U : Node → WithTop ℝ) (v : Node) (hv : v ∈ S) : bValue S U v ≤ U v
theorem
BanditRLProof.HOO.bValue_le_prefix_walk
Compiled
B is nondecreasing at every intermediate node on the actual chosen path.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.bValue_le_prefix_walkReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bValue_le_prefix_walk (S : Finset Node) (U : Node → WithTop ℝ) (k : ℕ) (v w : Node) (hvw : v <+: w) (hw : w <+: walk S (bValue S U) k v) : bValue S U v ≤ bValue S U w
theorem
BanditRLProof.HOO.visits_pos_mem_expanded
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.visits_pos_mem_expandedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem visits_pos_mem_expanded (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) (v : Node) (ht : 0 < visits (history ν ρ Y n) v) : v ∈ expanded (history ν ρ Y n)