BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityAllHorizon

Regime in which every component of the exact double-variance exploration schedule is at most one half.

def doubleVarianceProbabilisticSparseLossLargeHorizonCondition (K S T delta : Real) : Prop

All-horizon threshold for the exact double-variance sparse route: use the refined threshold in its valid regime and strict `T + 1` otherwise.

noncomputable def doubleVarianceProbabilisticSparseLossAllHorizonRegretThreshold {Action : Type v} (arms : Finset Action) (horizon sparsity : Nat) (delta : Real) : Real

Generated all-horizon exact double-variance regret away from the common sparsity-failure event. Both branches use the same eta, gamma, and measure.

theorem sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossRealizedRegret_tail_off_sparsityFailure {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) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (doubleVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu ({sample | doubleVarianceProbabilisticSparseLossAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} \ sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal delta

Generated all-horizon exact double-variance regret with the common sparsity-failure residual.

theorem sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (doubleVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | doubleVarianceProbabilisticSparseLossAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta + mu (sampledPredictableSparsityFailure arms loss horizon sparsity)

Practical all-horizon `delta + epsilon` theorem under the exact same-measure sparsity-failure bound.

theorem sampledPredictable_allHorizonDoubleVarianceProbabilisticSparseLossRealizedRegret_tail_of_sparsityFailure_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) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (doubleVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon → mu {sample | doubleVarianceProbabilisticSparseLossAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta + ENNReal.ofReal epsilon