BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityTuning

Complete Hedge scale using sparse loss mass and sparse pathwise variance.

noncomputable def pathwiseVarianceProbabilisticSparseLossHighProbabilityScale {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real

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

theorem pathwiseVarianceProbabilisticSparseLossHighProbabilityScale_pos {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : 0 < pathwiseVarianceProbabilisticSparseLossHighProbabilityScale arms gamma horizon sparsity delta

Learning rate balancing entropy against the four-event sparse scale.

noncomputable def pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real

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

theorem pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate_pos {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : 0 < pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta

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

theorem pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate_sq_mul_scale {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta ^ 2 * pathwiseVarianceProbabilisticSparseLossHighProbabilityScale arms gamma horizon sparsity delta = Real.log (arms.card : Real)

Under `gamma ≤ 1/2`, entropy and stability cost at most three balanced copies of the four-event sparse scale.

theorem pathwiseVarianceProbabilisticSparseLossHighProbabilityHedgeBudget_le_three_mul_sqrt {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : Real.log (arms.card : Real) / pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta + (pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta * (1 / (1 - gamma))) * pathwiseVarianceProbabilisticSparseLossHighProbabilityScale arms gamma horizon sparsity delta ≤ 3 * Real.sqrt (Real.log (arms.card : Real) * pathwiseVarianceProbabilisticSparseLossHighProbabilityScale arms gamma horizon sparsity delta)

Tuned regret threshold for the four-event pathwise-variance route.

noncomputable def pathwiseVarianceProbabilisticSparseLossRealizedTunedThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real

The raw four-event budget is bounded by the eta-tuned threshold.

theorem sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget_le_tunedThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget arms (pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta) gamma horizon sparsity delta ≤ pathwiseVarianceProbabilisticSparseLossRealizedTunedThreshold arms gamma horizon sparsity delta

Eta-tuned generated regret away from the exact sparsity-failure event.

theorem sampledPredictable_tunedProbabilisticSparseLossPathwiseVarianceRealizedRegret_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) : 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 | pathwiseVarianceProbabilisticSparseLossRealizedTunedThreshold 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

Eta-tuned generated regret with the exact sparsity-failure residual and the sparse pathwise variance budget.

theorem sampledPredictable_tunedProbabilisticSparseLossPathwiseVarianceRealizedRegret_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) : 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 | pathwiseVarianceProbabilisticSparseLossRealizedTunedThreshold 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 eta-tuned `delta + epsilon` theorem under the exact internally tuned generated measure.

theorem sampledPredictable_tunedProbabilisticSparseLossPathwiseVarianceRealizedRegret_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) : 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 | pathwiseVarianceProbabilisticSparseLossRealizedTunedThreshold 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