Lean module · EXP3
BanditRLProof.Exp3BernsteinRealizedHighProbabilityRegret
This module composes the generated predictable Bernstein-radius EXP3 theorem with the one-sided realized-minus-exploration deviation tail. The two importance-weighted confidence events use the variance-sensitive fixed-tilt route; the realized-deviation event retains its bounded-loss Hoeffding/Azuma radius. The deterministic Hedge-square contribution also remains unchanged.
Module map
Imports
BanditRLProof.Exp3BernsteinHighProbabilityRegret, BanditRLProof.Exp3RealizedConfidence
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.sampledPredictableBernsteinRealizedHighProbabilityRegretBudget
Compiled
Realized selected-loss regret budget whose predictable component uses the two variance-sensitive Bernstein confidence radii.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictableBernsteinRealizedHighProbabilityRegretBudgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sampledPredictableBernsteinRealizedHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinRealizedHighProbabilityRegret_tail_delta
Compiled
Raw three-event form. The predictable component contributes the pure-cross and fixed-comparator Bernstein events, while the third event is the bounded realized-minus-predictable deviation.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictable_bernsteinRealizedHighProbabilityRegret_tail_deltaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampledPredictable_bernsteinRealizedHighProbabilityRegret_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) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableBernsteinRealizedHighProbabilityRegretBudget arms eta gamma horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= (ENNReal.ofReal delta + ENNReal.ofReal delta) + ENNReal.ofReal delta
theorem
BanditRLProof.Exp3.sampledPredictable_bernsteinRealizedHighProbabilityRegret_tail_total_delta
Compiled
Total-failure form: the pure-cross Bernstein, fixed-comparator Bernstein, and realized-deviation events each receive `delta / 3`.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictable_bernsteinRealizedHighProbabilityRegret_tail_total_deltaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampledPredictable_bernsteinRealizedHighProbabilityRegret_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) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableBernsteinRealizedHighProbabilityRegretBudget arms eta gamma horizon (delta / 3) <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta