Lean module · Foundations
BanditRLProof.Regret
The first layer records pseudo-regret as an executable recursive object over finite arms and rational means. Later Mathlib-heavy files can connect this to expectations, conditional distributions, martingales, or concentration.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETC, BanditRLProof.Algorithms.Thompson, BanditRLProof.Algorithms.UCB, BanditRLProof.ConditionalExpectationReward, BanditRLProof.LeafLemmas
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.pseudoRegret
Compiled
Pseudo-regret accumulated from the model gaps along an action trace.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.pseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def pseudoRegret (model : FiniteBanditModel K) (action : Nat → Fin K) : Nat → Rat | 0 => 0 | t + 1 => pseudoRegret model action t + model.gap (action t) @[simp] theorem pseudoRegret_zero (model : FiniteBanditModel K) (action : Nat → Fin K) : pseudoRegret model action 0 = 0
theorem
BanditRLProof.pseudoRegret_zero
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.pseudoRegret_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem pseudoRegret_zero (model : FiniteBanditModel K) (action : Nat → Fin K) : pseudoRegret model action 0 = 0
theorem
BanditRLProof.pseudoRegret_succ
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.pseudoRegret_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem pseudoRegret_succ (model : FiniteBanditModel K) (action : Nat → Fin K) (t : Nat) : pseudoRegret model action (t + 1) = pseudoRegret model action t + model.gap (action t)
structure
BanditRLProof.RegretBoundCard
Compiled
A reusable record for theorem-card style regret bounds.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.RegretBoundCardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure RegretBoundCard where
structure
BanditRLProof.RegretObligation
Compiled
A proof obligation attached to a regret theorem.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.RegretObligationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure RegretObligation where