BanditRLProof.Exp3DoubleVarianceSparseBestArmEventualRefinedRegret

No declaration docstring is present; use the chapter context and exact statement below.

private theorem eventually_const_le_natCast (c : Real) : ∀ᶠ n : Nat in atTop, c <= (n : Real)

No declaration docstring is present; use the chapter context and exact statement below.

private theorem eventually_const_le_natCast_pow_three (c : Real) : ∀ᶠ n : Nat in atTop, c <= (n : Real) ^ 3

Every fixed choice of the four real-valued scale parameters eventually satisfies the deterministic large-horizon inequalities.

theorem eventually_doubleVarianceProbabilisticSparseLossLargeHorizonCondition (K S delta : Real) : ∀ᶠ horizon : Nat in atTop, doubleVarianceProbabilisticSparseLossLargeHorizonCondition K S (horizon : Real) delta

On the large-horizon branch, the best-arm all-horizon threshold is exactly the existing explicit double-variance threshold `16 * gamma * horizon`.

theorem doubleVarianceProbabilisticSparseLossBestArmAllHorizonRegretThreshold_eq_explicit_of_largeHorizon {Action : Type*} (arms : Finset Action) (horizon sparsity : Nat) (delta : Real) (hlarge : doubleVarianceProbabilisticSparseLossLargeHorizonCondition (arms.card : Real) (sparsity : Real) (horizon : Real) (delta / (arms.card : Real))) : doubleVarianceProbabilisticSparseLossBestArmAllHorizonRegretThreshold arms horizon sparsity delta = pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms (doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) (delta / (arms.card : Real))) horizon sparsity (delta / (arms.card : Real))

Pointwise off-sparsity tail with the explicit threshold, obtained without changing the generated trajectory measure selected by the parent theorem.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_off_sparsityFailure_of_largeHorizon {Env Action : Type*} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : MeasureTheory.Measure Env) [MeasureTheory.IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge : doubleVarianceProbabilisticSparseLossLargeHorizonCondition (arms.card : Real) (sparsity : Real) (horizon : Real) (delta / (arms.card : Real))) : let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu ({sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} \ sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal delta

Pointwise residual tail with the explicit threshold. The sparsity-failure term is retained exactly as in the all-horizon parent theorem.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_largeHorizon {Env Action : Type*} [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) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge : doubleVarianceProbabilisticSparseLossLargeHorizonCondition (arms.card : Real) (sparsity : Real) (horizon : Real) (delta / (arms.card : Real))) : let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta + mu (sampledPredictableSparsityFailure arms loss horizon sparsity)

Pointwise practical tail after supplying an outer-measure bound for the sparsity-failure event.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_sparsityFailure_le_of_largeHorizon {Env Action : Type*} [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) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge : doubleVarianceProbabilisticSparseLossLargeHorizonCondition (arms.card : Real) (sparsity : Real) (horizon : Real) (delta / (arms.card : Real))) : let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon -> mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta + ENNReal.ofReal epsilon

Eventually, every positive horizon has the explicit off-sparsity tail. Each horizon retains its own internally selected rates and trajectory measure.

theorem eventually_sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_off_sparsityFailure {Env Action : Type*} [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) (sparsity : Nat) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : ∀ᶠ horizon : Nat in atTop, 0 < horizon ∧ ∀ hhorizon : 0 < horizon, let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu ({sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} \ sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal delta

Eventually, every positive horizon has the explicit residual tail. This is an at-top statement about horizon-indexed measures, not an anytime event.

theorem eventually_sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail {Env Action : Type*} [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) (sparsity : Nat) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : ∀ᶠ horizon : Nat in atTop, 0 < horizon ∧ ∀ hhorizon : 0 < horizon, let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta + mu (sampledPredictableSparsityFailure arms loss horizon sparsity)

Eventually, an external sparsity-failure bound yields the explicit practical tail under the same horizon-indexed generated trajectory measures.

theorem eventually_sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossBestArmRealizedRegret_tail_of_sparsityFailure_le {Env Action : Type*} [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) (sparsity : Nat) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : ∀ᶠ horizon : Nat in atTop, 0 < horizon ∧ ∀ hhorizon : 0 < horizon, let deltaArm := delta / (arms.card : Real) let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity deltaArm let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) deltaArm (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) deltaArm).trans (by norm_num)) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon -> mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity deltaArm <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - sampledPredictableBestArmCumulativeLoss arms harms loss horizon sample} <= ENNReal.ofReal delta + ENNReal.ofReal epsilon