BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityExplicitTuning

Exploration scale forced by the exact selected-loss predictable-variance radius with budget `S * T`.

noncomputable def doubleVarianceProbabilisticSparseLossRealizedExplorationScale (S T delta : Real) : Real

The previous pathwise raw schedule augmented by the exact selected-loss predictable-variance scale.

noncomputable def doubleVarianceProbabilisticSparseLossRawExplorationRate (K S T delta : Real) : Real

Explicit double-variance exploration schedule clipped into the Hedge stability regime.

noncomputable def doubleVarianceProbabilisticSparseLossClippedExplorationRate (K S T delta : Real) : Real

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

theorem doubleVarianceProbabilisticSparseLossClippedExplorationRate_le_half (K S T delta : Real) : doubleVarianceProbabilisticSparseLossClippedExplorationRate K S T delta <= 1 / 2

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

theorem doubleVarianceProbabilisticSparseLossClippedExplorationRate_eq_raw (K S T delta : Real) (hraw : doubleVarianceProbabilisticSparseLossRawExplorationRate K S T delta <= 1 / 2) : doubleVarianceProbabilisticSparseLossClippedExplorationRate K S T delta = doubleVarianceProbabilisticSparseLossRawExplorationRate K S T delta

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

theorem doubleVarianceProbabilisticSparseLossRawExplorationRate_pos (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) : 0 < doubleVarianceProbabilisticSparseLossRawExplorationRate K S T delta

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

theorem doubleVarianceProbabilisticSparseLossClippedExplorationRate_pos (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) : 0 < doubleVarianceProbabilisticSparseLossClippedExplorationRate K S T delta

The selected-loss horizon contract also controls the older bounded realized-deviation component retained by the shared raw schedule.

theorem boundedRealizedLargeHorizon_of_doubleVarianceLargeHorizon (S T delta : Real) (hS_one : 1 <= S) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_realized : 4 * (S * Real.log (4 / delta)) <= T) : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= T

Four horizon contracts place every component of the double-variance raw schedule below one half.

theorem doubleVarianceProbabilisticSparseLossRawExplorationRate_le_half_of_horizon_contracts (K S T delta : Real) (hK_one : 1 < K) (hS_one : 1 <= S) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * (S * Real.log K) <= T) (hlarge_mixed : 32 * (K * S * Real.log K ^ 2 * Real.log (4 / delta)) <= T ^ 3) (hlarge_confidence : 8 * (K * Real.log (4 / delta)) <= T) (hlarge_realized : 4 * (S * Real.log (4 / delta)) <= T) : doubleVarianceProbabilisticSparseLossRawExplorationRate K S T delta <= 1 / 2

The clipped schedule supplies the base, mixed-square, Bernstein, and selected-loss predictable-variance contracts.

theorem doubleVarianceProbabilisticSparseLossClippedExplorationRate_contracts (K S T delta : Real) (hK_one : 1 < K) (hS_one : 1 <= S) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * (S * Real.log K) <= T) (hlarge_mixed : 32 * (K * S * Real.log K ^ 2 * Real.log (4 / delta)) <= T ^ 3) (hlarge_confidence : 8 * (K * Real.log (4 / delta)) <= T) (hlarge_realized : 4 * (S * Real.log (4 / delta)) <= T) : let gamma := doubleVarianceProbabilisticSparseLossClippedExplorationRate K S T delta 0 < gamma ∧ gamma <= 1 / 2 ∧ S * Real.log K <= gamma ^ 2 * T ∧ K * S * Real.log K ^ 2 * Real.log (4 / delta) <= gamma ^ 5 * T ^ 3 ∧ K * Real.log (4 / delta) <= gamma ^ 3 * T ∧ S * Real.log (4 / delta) <= gamma ^ 2 * T

Explicit double-variance threshold after tuning eta and gamma.

noncomputable def pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold {Action : Type v} (_arms : Finset Action) (gamma : Real) (horizon _sparsity : Nat) (_delta : Real) : Real

The exact selected-loss predictable-variance radius is at most `3 * gamma * T` under its sparse variance contract.

theorem sparseRealizedPredictableVarianceRadius_le_three_mul_gamma_mul_horizon (S T gamma delta : Real) (hS_one : 1 <= S) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrealized : S * Real.log (4 / delta) <= gamma ^ 2 * T) : sampledRealizedPredictableVarianceRadius (S * T) (delta / 4) <= 3 * gamma * T

The four exploration contracts reduce the eta-tuned double-variance threshold to `16 * gamma * T`.

theorem pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedTunedThreshold_le_explicitThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 <= arms.card) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (gamma delta : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) <= gamma ^ 5 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : (sparsity : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedTunedThreshold arms gamma horizon sparsity delta <= pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma horizon sparsity delta

Gamma-characterized double-variance regret tail away from the exact sparsity-failure event.

theorem sampledPredictable_gammaCharacterizedDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (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) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) <= gamma ^ 5 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : (sparsity : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu ({sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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

Gamma-characterized double-variance regret with the exact sparsity-failure residual.

theorem sampledPredictable_gammaCharacterizedDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (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) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) <= gamma ^ 5 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : (sparsity : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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 gamma-characterized endpoint under the exact generated-measure bound on the sparsity-failure event.

theorem sampledPredictable_gammaCharacterizedDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (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) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) <= gamma ^ 5 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : (sparsity : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon → mu {sample | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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

Fully explicit double-variance regret tail away from the exact sparsity-failure event for the clipped schedule.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (hlarge_arm : 4 * ((sparsity : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_mixed : 32 * ((arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta)) <= (horizon : Real) ^ 3) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (4 / delta)) <= (horizon : Real)) (hlarge_realized : 4 * ((sparsity : Real) * Real.log (4 / delta)) <= (horizon : Real)) : 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 | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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

Fully explicit double-variance regret with the exact sparsity-failure residual.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (hlarge_arm : 4 * ((sparsity : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_mixed : 32 * ((arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta)) <= (horizon : Real) ^ 3) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (4 / delta)) <= (horizon : Real)) (hlarge_realized : 4 * ((sparsity : Real) * Real.log (4 / delta)) <= (horizon : Real)) : 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 | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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)

Fully explicit practical `delta + epsilon` theorem under the exact sparsity-failure bound for the internally eta/gamma-tuned measure.

theorem sampledPredictable_explicitDoubleVarianceProbabilisticSparseLossRealizedRegret_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) (hlarge_arm : 4 * ((sparsity : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_mixed : 32 * ((arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta)) <= (horizon : Real) ^ 3) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (4 / delta)) <= (horizon : Real)) (hlarge_realized : 4 * ((sparsity : Real) * Real.log (4 / delta)) <= (horizon : Real)) : 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 | pathwiseVarianceProbabilisticSparseLossDoubleVarianceRealizedExplicitThreshold arms gamma 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