Lean module · EXP3
BanditRLProof.Exp3BernsteinRealizedHighProbabilityRegret
# Generated realized EXP3 regret with Bernstein predictable confidence 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. Thus the endpoint controls generated selected scalar loss, but it is not a general Freedman theorem or an ideal tuned EXP3.P rate.
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.
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.
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`.
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