BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityRegretRate

The complete scalar budget displayed by the power-of-two forced tail.

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

Increasing the outer confidence budget decreases the explicit telescoping confidence logarithm.

theorem telescopingHighProbabilityRegretLogBudget_anti_delta {Feature : Type u} [Fintype Feature] (lambda L2 : Real) {deltaSmall deltaLarge : Real} (hdeltaSmall : 0 < deltaSmall) (hdelta : deltaSmall <= deltaLarge) (horizon : Nat) : telescopingHighProbabilityRegretLogBudget (Feature

For fixed positive `delta`, the explicit telescoping confidence logarithm is `O(log (T + 1))`.

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

For fixed model parameters and confidence level, the explicit telescoping high-probability budget is `O(sqrt (T + 1) * log (T + 1))`.

theorem telescopingHighProbabilityPseudoRegretBound_isBigO_sqrt_mul_log {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 => telescopingHighProbabilityPseudoRegretBound (Feature

The cast of `Nat.log2 T + 1` is `O(log (T + 1))`.

theorem natCast_log2_add_one_isBigO_log_succ : (fun horizon : Nat => ((Nat.log2 horizon + 1 : Nat) : Real)) =O[atTop] (fun horizon : Nat => Real.log (((horizon + 1 : Nat) : Real)))

The exact scalar power-of-two forced budget is `O(sqrt (T + 1) * log (T + 1))`.

theorem powerOfTwoForcedScalarHighProbabilityPseudoRegretBound_isBigO_sqrt_mul_log {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

Named all-horizon violation event for the exact scalar asymptotic budget.

noncomputable def powerOfTwoForcedCanonicalAsymptoticHighProbabilityPseudoRegretAllHorizonViolationSet {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) : Set (Nat -> Fin K × Real)

The asymptotic wrapper uses exactly the compiled scalar violation event.

theorem powerOfTwoForcedCanonicalAsymptoticHighProbabilityPseudoRegretAllHorizonViolationSet_eq_scalar {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) : powerOfTwoForcedCanonicalAsymptoticHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best = powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegretScalarAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best

Complete one-policy asymptotic high-probability theorem: the exact scalar budget has the displayed fixed-model Big-O rate, complete pseudo-regret is nonnegative, and the unchanged all-horizon violation event has probability at most `delta`.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegret_asymptoticRate_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) : ((fun horizon : Nat => powerOfTwoForcedScalarHighProbabilityPseudoRegretBound (Feature