Lean module · EXP3
BanditRLProof.Exp3RealizedHighProbabilityRegret
# Generated realized EXP3 high-probability regret 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. The theorem inherits the range-based importance-weighted confidence radii from the predictable route. It is therefore a valid realized selected-loss theorem, but it is not presented as the ideal EXP3.P/Freedman rate.
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.
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.
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`.
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