Lean module · Foundations
BanditRLProof.Core
# Core bandit vocabulary This file keeps the first project layer dependency-light. It provides a small executable language for finite action traces, pull counts, reward sums, and finite-arm mean models. Strong probabilistic statements can later import Mathlib or external libraries without changing this public surface.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCMeasurability, BanditRLProof.Algorithms.ETCTrace, BanditRLProof.FiniteBanditModelInvariants, BanditRLProof.IndependenceFoundation, BanditRLProof.MeasureFoundation, BanditRLProof.Regret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
abbrev
BanditRLProof.ActionTrace
Compiled
A sequence of actions chosen by a bandit algorithm.
abbrev ActionTrace (Action : Type u)
abbrev
BanditRLProof.RewardTrace
Compiled
A sequence of observed rewards.
abbrev RewardTrace (Reward : Type v)
def
BanditRLProof.pullCount
Compiled
Number of pulls of action `a` before time `t`.
def pullCount [DecidableEq Action] (action : ActionTrace Action) (a : Action) : Nat → Nat | 0 => 0 | t + 1 => pullCount action a t + if action t = a then 1 else 0 @[simp] theorem pullCount_zero [DecidableEq Action] (action : ActionTrace Action) (a : Action) : pullCount action a 0 = 0
theorem
BanditRLProof.pullCount_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem pullCount_zero [DecidableEq Action] (action : ActionTrace Action) (a : Action) : pullCount action a 0 = 0
theorem
BanditRLProof.pullCount_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem pullCount_succ [DecidableEq Action] (action : ActionTrace Action) (a : Action) (t : Nat) : pullCount action a (t + 1) = pullCount action a t + if action t = a then 1 else 0
def
BanditRLProof.sumRewards
Compiled
Sum of rewards obtained from action `a` before time `t`.
def sumRewards [DecidableEq Action] [OfNat Reward 0] [HAdd Reward Reward Reward] (action : ActionTrace Action) (reward : RewardTrace Reward) (a : Action) : Nat → Reward | 0 => 0 | t + 1 => sumRewards action reward a t + if action t = a then reward t else 0 @[simp] theorem sumRewards_zero [DecidableEq Action] [OfNat Reward 0] [HAdd Reward Reward Reward] (action : ActionTrace Action) (reward : RewardTrace Reward) (a : Action) : sumRewards action reward a 0 = 0
theorem
BanditRLProof.sumRewards_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem sumRewards_zero [DecidableEq Action] [OfNat Reward 0] [HAdd Reward Reward Reward] (action : ActionTrace Action) (reward : RewardTrace Reward) (a : Action) : sumRewards action reward a 0 = 0
theorem
BanditRLProof.sumRewards_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem sumRewards_succ [DecidableEq Action] [OfNat Reward 0] [HAdd Reward Reward Reward] (action : ActionTrace Action) (reward : RewardTrace Reward) (a : Action) (t : Nat) : sumRewards action reward a (t + 1) = sumRewards action reward a t + if action t = a then reward t else 0
structure
BanditRLProof.FiniteBanditModel
Compiled
A finite stochastic bandit model represented by the mean reward of each arm.
structure FiniteBanditModel (K : Nat) where
def
BanditRLProof.FiniteBanditModel.bestArm
Compiled
A computable argmax-style selector for the best arm.
noncomputable def bestArm (model : FiniteBanditModel K) : Fin K
def
BanditRLProof.FiniteBanditModel.bestMean
Compiled
The mean reward of `bestArm`.
noncomputable def bestMean (model : FiniteBanditModel K) : Rat
def
BanditRLProof.FiniteBanditModel.gap
Compiled
The gap of an arm relative to the selected best arm.
noncomputable def gap (model : FiniteBanditModel K) (arm : Fin K) : Rat
theorem
BanditRLProof.FiniteBanditModel.gap_bestArm
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem gap_bestArm (model : FiniteBanditModel K) : model.gap model.bestArm = 0
structure
BanditRLProof.PolicySketch
Compiled
A named policy surface that agents can map to a concrete Lean definition.
structure PolicySketch (K : Nat) where
inductive
BanditRLProof.CertificateStatus
Compiled
Status of a theorem or candidate in the harness memory.
inductive CertificateStatus where