Lean module · EXP3
BanditRLProof.Exp3RealizedConfidence
# Delta-shaped confidence for realized EXP3 deviation This module converts the finite-horizon ENNReal Azuma bound into an explicit square-root confidence radius. It closes the one-sided confidence theorem for realized loss minus the exploration-mixed predictable conditional mean; it does not identify the estimator-valued Hedge comparator with true comparator loss.
Module map
Imports
BanditRLProof.Exp3RealizedDeviationTail
Imported by
BanditRLProof, BanditRLProof.Exp3BernsteinRealizedHighProbabilityRegret, BanditRLProof.Exp3MixedSquareBernsteinRealizedHighProbabilityRegret, BanditRLProof.Exp3MixedSquareExponentialRealizedHighProbabilityRegret, BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedHighProbabilityRegret, BanditRLProof.Exp3RandomSquareBernsteinRealizedHighProbabilityRegret, BanditRLProof.Exp3RealizedHighProbabilityRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableRealizedDeviationConfidenceRadius
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableRealizedDeviationConfidenceRadius (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.intervalVarianceProxy_zero_one_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem intervalVarianceProxy_zero_one_pos : 0 < ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real)
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviationConfidenceRadius_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviationConfidenceRadius_nonneg (horizon : Nat) (delta : Real) : 0 <= sampledPredictableRealizedDeviationConfidenceRadius horizon delta
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviationConfidenceRadius_sq_domination
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviationConfidenceRadius_sq_domination (horizon : Nat) (budget : Real) : 2 * ((((horizon : NNReal) * Concentration.intervalVarianceProxy 0 1 : NNReal)) : Real) * budget <= (Real.sqrt (2 * ((((horizon : NNReal) * Concentration.intervalVarianceProxy 0 1 : NNReal)) : Real) * budget)) ^ 2
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_exp_neg_budget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviation_sum_tail_exp_neg_budget {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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (budget : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment mu {sample | Real.sqrt (2 * ((((horizon : NNReal) * Concentration.intervalVarianceProxy 0 1 : NNReal)) : Real) * budget) <= (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-budget))
theorem
BanditRLProof.Exp3.sampledPredictableRealizedDeviation_sum_tail_delta
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledPredictableRealizedDeviation_sum_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) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment mu {sample | sampledPredictableRealizedDeviationConfidenceRadius horizon delta <= (Finset.range horizon).sum (fun i => sampledTrajectoryRealizedDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal delta