Lean module · EXP3
BanditRLProof.Exp3RealizedHighProbabilityRegret
This module composes the generated predictable EXP3 high-probability theorem with the one-sided realized-minus-exploration-mixed deviation tail. The primary endpoint controls the scalar loss stored in the generated trajectory, with the requested total failure probability split equally across the pure-q, comparator-estimator, and realized-deviation events.
Module map
Imports
BanditRLProof.Exp3HighProbabilityRegret, 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.sampledPredictableRealizedHighProbabilityRegretBudget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictableRealizedHighProbabilityRegretBudgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sampledPredictableRealizedHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_realizedHighProbabilityRegret_tail_delta
Compiled
Raw three-event form of the generated realized EXP3 regret theorem. The same `delta` is used for the pure-q, comparator-estimator, and realized deviation tails, so the displayed failure probability is their three-term sum.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictable_realizedHighProbabilityRegret_tail_deltaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampledPredictable_realizedHighProbabilityRegret_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 | sampledPredictableRealizedHighProbabilityRegretBudget 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_realizedHighProbabilityRegret_tail_total_delta
Compiled
Standard total-failure-probability form of generated realized EXP3 regret. Each of the three underlying confidence events receives `delta / 3`.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictable_realizedHighProbabilityRegret_tail_total_deltaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampledPredictable_realizedHighProbabilityRegret_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 | sampledPredictableRealizedHighProbabilityRegretBudget 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