Lean module · Foundations
BanditRLProof.Regret
# Regret surfaces 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.
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.
@[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.
@[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.
structure RegretBoundCard where
structure
BanditRLProof.RegretObligation
Compiled
A proof obligation attached to a regret theorem.
structure RegretObligation where