Lean module · EXP3
BanditRLProof.Exp3RealizedPredictableVarianceAllTime
# All-time realized EXP3 predictable-variance tail This module gives every positive prefix of one fixed generated EXP3 process a geometric confidence share. The resulting countable union is controlled by one outer confidence budget. This is countable outer-measure subadditivity, not a Ville/Doob, mixture, optional-stopping, self-normalized, or general Freedman theorem.
Module map
Imports
BanditRLProof.ConcentrationQuadraticScheduled, BanditRLProof.ConcentrationConfidenceSchedule, 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.sampledRealizedPredictableVarianceGeometricRadius
Compiled
The selected-loss predictable-variance radius at prefix `n+1` under the geometric confidence schedule.
noncomputable def sampledRealizedPredictableVarianceGeometricRadius (varianceBudget : Nat -> Real) (delta : Real) (n : Nat) : Real
def
BanditRLProof.Exp3.sampledPredictableRealizedDeviationAllTimeFailureSet
Compiled
Countable failure event over every positive prefix of one generated EXP3 trajectory.
noncomputable def sampledPredictableRealizedDeviationAllTimeFailureSet {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (varianceBudget : Nat -> Real) (delta : Real) : Set (Env × ((k : Nat) -> Action × Real))
theorem
BanditRLProof.Exp3.mem_sampledPredictableRealizedDeviationAllTimeFailureSet_iff
Compiled
Membership is failure at at least one positive prefix.
theorem mem_sampledPredictableRealizedDeviationAllTimeFailureSet_iff {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (varianceBudget : Nat -> Real) (delta : Real) (sample : Env × ((k : Nat) -> Action × Real)) : sample ∈ sampledPredictableRealizedDeviationAllTimeFailureSet arms eta gamma loss varianceBudget delta ↔ ∃ n, sampledRealizedPredictableVarianceGeometricRadius varianceBudget delta n <= (Finset.range (n + 1)).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample) ∧ (Finset.range (n + 1)).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) <= varianceBudget n
theorem
BanditRLProof.Exp3.measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le
Compiled
On one generated EXP3 trajectory law, the joint deviation/predictable-variance failures over all positive prefixes have total mass at most the outer confidence budget.
theorem measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le {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) (varianceBudget : Nat -> Real) (hvarianceBudget : forall n, 0 < varianceBudget n) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu (sampledPredictableRealizedDeviationAllTimeFailureSet arms eta gamma loss varianceBudget delta) <= ENNReal.ofReal delta