BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityAverageRegret

The exact scalar power-of-two forced high-probability budget is `o(T + 1)` for fixed model parameters and fixed positive outer confidence budget.

theorem powerOfTwoForcedScalarHighProbabilityPseudoRegretBound_isLittleO_natCast_succ {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (delta : Real) (hdelta : 0 < delta) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (L2 : Real) (hL2 : 0 <= L2) : (fun horizon : Nat => powerOfTwoForcedScalarHighProbabilityPseudoRegretBound (Feature

The exact scalar high-probability budget per available round.

noncomputable def powerOfTwoForcedScalarHighProbabilityAveragePseudoRegretBound {Feature : Type u} [Fintype Feature] (R delta lambda S : Real) (horizon : Nat) (L2 : Real) : Real

The exact scalar high-probability budget per round converges to zero.

theorem powerOfTwoForcedScalarHighProbabilityAveragePseudoRegretBound_tendsto_zero {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (delta : Real) (hdelta : 0 < delta) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (L2 : Real) (hL2 : 0 <= L2) : Tendsto (powerOfTwoForcedScalarHighProbabilityAveragePseudoRegretBound (Feature

Complete fixed-best pseudo-regret per available round.

noncomputable def powerOfTwoForcedCanonicalStandardHighProbabilityAveragePseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (horizon : Nat) (trajectory : Nat -> Fin K × Real) : Real

Outside the named all-horizon violation event, complete pseudo-regret per round is bounded by the exact scalar average budget at every horizon.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityAveragePseudoRegret_le_averageBound_of_not_mem_allHorizonViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (best : Fin K) (trajectory : Nat -> Fin K × Real) (hnot : trajectory ∉ powerOfTwoForcedCanonicalAsymptoticHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best) (horizon : Nat) : powerOfTwoForcedCanonicalStandardHighProbabilityAveragePseudoRegret thetaStar actionFeature best horizon trajectory <= powerOfTwoForcedScalarHighProbabilityAveragePseudoRegretBound (Feature

Complete fixed-model average-envelope theorem for one power-of-two forced policy: the exact scalar average budget tends to zero, it bounds complete pseudo-regret per round outside the unchanged all-horizon event, pseudo-regret is nonnegative, and the event has probability at most `delta`.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegret_averageBudget_tendsto_zero_nonneg_and_allHorizon_tail_le_of_linearSubgaussianEnvironment_of_featureBound_le_regularization {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Tendsto (powerOfTwoForcedScalarHighProbabilityAveragePseudoRegretBound (Feature