Lean module · EXP3
BanditRLProof.Exp3RandomSquareBernsteinRealizedHighProbabilityRegret
# Generated realized EXP3 regret with a random estimator-square event This module composes the generated predictable random-square Bernstein theorem with the one-sided realized-minus-exploration deviation tail. The resulting four-event route controls generated selected scalar loss while preserving the random `|arms| * T / deltaSquare` Hedge-square budget. The Markov square event still costs `1 / deltaSquare`, both importance-weighted Bernstein radii retain exploration-floor dependence, and the realized deviation uses the bounded-loss Hoeffding/Azuma radius. This is therefore not an ideal EXP3.P or Freedman-rate theorem.
Module map
Imports
BanditRLProof.Exp3RandomSquareHighProbabilityRegret, BanditRLProof.Exp3RealizedConfidence
Imported by
BanditRLProof, BanditRLProof.Exp3RandomSquareBernsteinRealizedTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget
Compiled
Realized selected-loss regret budget whose predictable component uses the random estimator-square event and two variance-sensitive Bernstein radii.
noncomputable def sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget {Action : Type v} (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (deltaSquare deltaConfidence deltaRealized : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_randomSquareBernsteinRealizedHighProbabilityRegret_tail
Compiled
Raw four-event form. The predictable component contributes the random estimator-square event and the two Bernstein confidence events; the fourth event is the bounded realized-minus-predictable deviation.
theorem sampledPredictable_randomSquareBernsteinRealizedHighProbabilityRegret_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) (hhorizon : 0 < horizon) (deltaSquare deltaConfidence deltaRealized : Real) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget arms eta gamma horizon deltaSquare deltaConfidence deltaRealized <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized
theorem
BanditRLProof.Exp3.sampledPredictable_randomSquareBernsteinRealizedHighProbabilityRegret_tail_total_delta
Compiled
Total-failure form: the estimator-square, pure-cross Bernstein, fixed-comparator Bernstein, and realized-deviation events each receive `delta / 4`.
theorem sampledPredictable_randomSquareBernsteinRealizedHighProbabilityRegret_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 | sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget arms eta gamma horizon (delta / 4) (delta / 4) (delta / 4) <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta