BanditRLProof.Exp3MixedSquarePredictableVarianceHighProbabilityRegret

The observed mixed estimator-square sum has a random predictable-variance tail on the event that the cumulative variance is at most `varianceBudget`.

theorem sampledPredictableObservedMixedSquared_sum_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) (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 {sample | (arms.card : Real) * (horizon : Real) + sampledMixedSquaredPredictableVarianceRadius arms gamma varianceBudget delta <= sampledObservedMixedSquaredSum arms eta gamma horizon sample ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) <= varianceBudget} <= ENNReal.ofReal delta

Predictable regret budget with a caller-supplied cumulative predictable variance budget.

noncomputable def sampledPredictableVarianceSquareHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (varianceBudget deltaSquare deltaConfidence : Real) : Real

Generated predictable EXP3 regret on the event that the cumulative predictable mixed-square variance stays below `varianceBudget`.

theorem sampledPredictable_predictableVarianceSquareHighProbabilityRegret_tail_joint {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) (varianceBudget deltaSquare deltaConfidence : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareHighProbabilityRegretBudget arms eta gamma horizon varianceBudget deltaSquare deltaConfidence <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss 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) <= varianceBudget} <= (ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence

Unconditional predictable-regret bound with the cumulative predictable variance overflow probability left explicit.

theorem sampledPredictable_predictableVarianceSquareHighProbabilityRegret_tail {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) (varianceBudget deltaSquare deltaConfidence : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareHighProbabilityRegretBudget arms eta gamma horizon varianceBudget deltaSquare deltaConfidence <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + mu {sample | varianceBudget < (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample)}

Total-failure joint-event form with the square, pure-cross, and comparator events allocated `delta / 3`.

theorem sampledPredictable_predictableVarianceSquareHighProbabilityRegret_tail_joint_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) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareHighProbabilityRegretBudget arms eta gamma horizon varianceBudget (delta / 3) (delta / 3) <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss 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) <= varianceBudget} <= ENNReal.ofReal delta

Primary residual-variance form: total confidence failure is `delta`, and the only remaining term is the probability that cumulative predictable variance exceeds `varianceBudget`.

theorem sampledPredictable_predictableVarianceSquareHighProbabilityRegret_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) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareHighProbabilityRegretBudget arms eta gamma horizon varianceBudget (delta / 3) (delta / 3) <= (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta + mu {sample | varianceBudget < (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample)}