Lean module · EXP3
BanditRLProof.Exp3RealizedPredictableVarianceMaximal
# Finite-prefix realized EXP3 predictable-variance tail This module applies the finite maximal quadratic fixed-MGF route to every positive prefix of the generated realized-loss deviation process.
Module map
Imports
BanditRLProof.ConcentrationQuadraticMaximal, BanditRLProof.Exp3RealizedPredictableVarianceTail
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.sampledRealizedPredictableVarianceMaximalRadius
Compiled
Equal-share radius for indices `t < horizon`, hence prefix lengths `1` through `horizon` inclusive.
noncomputable def sampledRealizedPredictableVarianceMaximalRadius (horizon : Nat) (varianceBudget delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_prefix_max_tail_predictableVariance_delta
Compiled
Finite maximal predictable-variance tail for the realized selected-loss deviation over every positive prefix of the generated EXP3 trajectory.
theorem sampledPredictableRealizedDeviation_prefix_max_tail_predictableVariance_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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu (⋃ t ∈ Finset.range horizon, {sample | sampledRealizedPredictableVarianceMaximalRadius horizon varianceBudget delta <= (Finset.range (t + 1)).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample) ∧ (Finset.range (t + 1)).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) <= varianceBudget}) <= ENNReal.ofReal delta