Lean module · Foundations
BanditRLProof.PullCountReindex
Generated source map for this Lean module.
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.sum_selected_pullCount
Compiled
Each selected round visits exactly one successive pre-pull count.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.sum_selected_pullCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_selected_pullCount {Action : Type*} [DecidableEq Action] (action : ActionTrace Action) (a : Action) (f : ℕ → ℝ) (T : ℕ) : (∑ t ∈ range T, if action t = a then f (pullCount action a t) else 0) = ∑ s ∈ range (pullCount action a T), f s
theorem
BanditRLProof.pullCount_le_one_add_eventCount
Compiled
Event-count transport retains the first pull, whose pre-pull count is zero. The event premise must be supplied separately by the algorithm analysis.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.pullCount_le_one_add_eventCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem pullCount_le_one_add_eventCount {Action : Type*} [DecidableEq Action] (action : ActionTrace Action) (a : Action) (P : ℕ → Prop) [DecidablePred P] (T : ℕ) (hselected : ∀ t < T, action t = a → 0 < pullCount action a t → P (pullCount action a t)) : (pullCount action a T : ℝ) ≤ 1 + ∑ s ∈ range T, if P (s + 1) then (1 : ℝ) else 0