BanditRLProof.Core

A sequence of actions chosen by a bandit algorithm.

abbrev ActionTrace (Action : Type u)

A sequence of observed rewards.

abbrev RewardTrace (Reward : Type v)

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

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

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

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

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

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

A finite stochastic bandit model represented by the mean reward of each arm.

structure FiniteBanditModel (K : Nat) where

A computable argmax-style selector for the best arm.

noncomputable def bestArm (model : FiniteBanditModel K) : Fin K

The mean reward of `bestArm`.

noncomputable def bestMean (model : FiniteBanditModel K) : Rat

The gap of an arm relative to the selected best arm.

noncomputable def gap (model : FiniteBanditModel K) (arm : Fin K) : Rat

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

A named policy surface that agents can map to a concrete Lean definition.

structure PolicySketch (K : Nat) where

Status of a theorem or candidate in the harness memory.

inductive CertificateStatus where