Lean module · EXP3
BanditRLProof.Exp3BernsteinHighProbabilityRegret
# Variance-sensitive predictable EXP3 high-probability regret This module reassembles the generated predictable EXP3 regret theorem with the variance-sensitive pure-cross and fixed-comparator confidence radii. The random Hedge-square contribution retains its existing pathwise reciprocal-floor bound; no general Freedman or predictable-variance theorem is claimed.
Module map
Imports
BanditRLProof.Exp3HighProbabilityRegret, BanditRLProof.Exp3PureBernstein
Imported by
BanditRLProof, BanditRLProof.Exp3BernsteinRealizedHighProbabilityRegret, BanditRLProof.Exp3RandomSquareHighProbabilityRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableBernsteinHighProbabilityRegretBudget
Compiled
Predictable generated-regret budget with variance-sensitive confidence radii and the existing pathwise estimator-square contribution.
noncomputable def sampledPredictableBernsteinHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinHighProbabilityRegret_tail_delta
Compiled
Generated predictable EXP3 regret with both importance-weighted confidence events using their variance-sensitive fixed-tilt routes.
theorem sampledPredictable_bernsteinHighProbabilityRegret_tail_delta {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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableBernsteinHighProbabilityRegretBudget arms eta gamma horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta + ENNReal.ofReal delta
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinHighProbabilityRegret_tail_total_delta
Compiled
Total-failure form: each variance-sensitive confidence event receives `delta / 2`. Unlike the range-Hoeffding predecessor, no positive-horizon premise is needed.
theorem sampledPredictable_bernsteinHighProbabilityRegret_tail_total_delta {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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableBernsteinHighProbabilityRegretBudget arms eta gamma horizon (delta / 2) <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta