Lean module · EXP3
BanditRLProof.Exp3MixedSquareBernsteinRealizedBestArmAllHorizon
# Best-arm all-horizon Bernstein mixed-square realized EXP3 This module upgrades the fixed-comparator all-horizon Bernstein mixed-square tail to the best supported arm in hindsight. The fixed-comparator schedule is calibrated at `delta / K`; all comparators share the same generated trajectory measure, so a finite union gives total failure probability at most `delta`.
Module map
Imports
BanditRLProof.Exp3BestArm, BanditRLProof.Exp3MixedSquareBernsteinRealizedAllHorizon
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.bernsteinSquareBestArmAllHorizonRegretThreshold
Compiled
Best-arm Bernstein mixed-square all-horizon threshold. The underlying fixed-comparator schedule receives the confidence share `delta / K`.
noncomputable def bernsteinSquareBestArmAllHorizonRegretThreshold {Action : Type v} (arms : Finset Action) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail
Compiled
Generated realized-regret tail against the best supported arm in hindsight for every positive horizon. The finite comparator union spends `delta / K` on each arm and therefore has total failure probability at most `delta`.
theorem sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let deltaArm := delta / (arms.card : Real) let gamma := bernsteinSquareClippedExplorationRate (arms.card : Real) (horizon : Real) deltaArm let eta := bernsteinSquareHighProbabilityLearningRate arms gamma horizon deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (bernsteinSquareClippedExplorationRate_pos (arms.card : Real) (horizon : Real) deltaArm (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (bernsteinSquareClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) deltaArm).trans (by norm_num)) loss.environment mu {sample | bernsteinSquareBestArmAllHorizonRegretThreshold arms horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta