Lean module · EXP3
BanditRLProof.Exp3BestArm
# Shared finite best-arm transport for EXP3 This module packages the comparator-independent order step used by finite-arm best-in-hindsight regret wrappers. It contains no probability bound: downstream routes identify the best-arm event with a finite union of fixed-comparator events and supply their own confidence schedules.
Module map
Imports
BanditRLProof.Exp3RealizedRegret
Imported by
BanditRLProof.Exp3MixedSquareBernsteinRealizedBestArmAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityBestArmAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityBestArmAllHorizon
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableBestArmCumulativeLoss
Compiled
Cumulative predictable loss of the best supported arm in hindsight.
noncomputable def sampledPredictableBestArmCumulativeLoss {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (harms : arms.Nonempty) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : Real
theorem
BanditRLProof.Exp3.threshold_le_sampledPredictableRealizedLoss_sub_bestArmCumulativeLoss_iff
Compiled
The best-arm regret event is exactly the finite existential union of the fixed-comparator regret events.
theorem threshold_le_sampledPredictableRealizedLoss_sub_bestArmCumulativeLoss_iff {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (harms : arms.Nonempty) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) (threshold : Real) : threshold <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample ↔ ∃ comparator ∈ arms, threshold <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)