Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedDoublePredictableVarianceHighProbabilityRegret
# Small-loss EXP3 regret with two predictable-variance budgets The predictable-regret component uses the armwise loss-mass budget and the mixed-square predictable variance. The realized-minus-predictable component uses its exact selected-loss predictable variance. An explicit bad set is retained so probabilistic sparsity can discharge both pathwise budgets without charging the same failure event more than once.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedMarkovHighProbabilityRegret, 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.sampledPredictableVarianceSquareSmallLossDoubleVarianceRealizedHighProbabilityRegretBudget
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
noncomputable def sampledPredictableVarianceSquareSmallLossDoubleVarianceRealizedHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (lossMassBudget mixedVarianceBudget realizedVarianceBudget deltaSquare deltaConfidence deltaRealized : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_smallLossDoublePredictableVarianceRealizedHighProbabilityRegret_tail_joint_off_bad_of_lossMassSum_le_or_mem
Compiled
Joint realized-regret tail away from an explicit loss-mass bad set, with simultaneous mixed-square and selected-loss predictable-variance budgets.
theorem sampledPredictable_smallLossDoublePredictableVarianceRealizedHighProbabilityRegret_tail_joint_off_bad_of_lossMassSum_le_or_mem {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) (lossMassBudget mixedVarianceBudget realizedVarianceBudget deltaSquare deltaConfidence deltaRealized : Real) (hmixedVarianceBudget : 0 < mixedVarianceBudget) (hrealizedVarianceBudget : 0 < realizedVarianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment, sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu ({sample | sampledPredictableVarianceSquareSmallLossDoubleVarianceRealizedHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget mixedVarianceBudget realizedVarianceBudget deltaSquare deltaConfidence deltaRealized ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator) ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ mixedVarianceBudget ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ realizedVarianceBudget} \ bad) ≤ ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized