Lean module · EXP3
BanditRLProof.Exp3MixedSquareBernsteinHighProbabilityRegret
# Predictable EXP3 regret with variance-sensitive mixed-square confidence This module consumes the generated mixed-square Bernstein tail in the existing three-event predictable-regret assembly. The square-event radius now uses the second-moment coefficient `K / epsilon`; the pure-cross and fixed-comparator events retain their compiled Bernstein radii.
Module map
Imports
BanditRLProof.Exp3MixedSquareBernstein, BanditRLProof.Exp3MixedSquareExponentialHighProbabilityRegret
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquareBernsteinRealizedHighProbabilityRegret, BanditRLProof.Exp3MixedSquarePredictableVarianceHighProbabilityRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableBernsteinSquareHighProbabilityRegretBudget
Compiled
Predictable regret budget using the variance-sensitive mixed-square Bernstein radius.
noncomputable def sampledPredictableBernsteinSquareHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (deltaSquare deltaConfidence : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinSquareHighProbabilityRegret_tail
Compiled
Generated predictable EXP3 regret with the mixed-square, pure-cross, and fixed-comparator Bernstein events.
theorem sampledPredictable_bernsteinSquareHighProbabilityRegret_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) (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) (deltaSquare deltaConfidence : Real) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableBernsteinSquareHighProbabilityRegretBudget arms eta gamma horizon deltaSquare deltaConfidence <= (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 deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinSquareHighProbabilityRegret_tail_total_delta
Compiled
Total-failure form with all three Bernstein events allocated `delta / 3`.
theorem sampledPredictable_bernsteinSquareHighProbabilityRegret_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 | sampledPredictableBernsteinSquareHighProbabilityRegretBudget arms eta gamma horizon (delta / 3) (delta / 3) <= (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