BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretRate

The explicit scheduled confidence logarithm after choosing the outer expected-regret budget `delta_T = 1 / (T + 1)`.

noncomputable def telescopingStandardExpectedRegretLogBudget {Feature : Type u} [Fintype Feature] (lambda : Real) (horizon : Nat) (L2 : Real) : Real

Substituting `delta_T = 1 / (T + 1)` into the scheduled confidence logarithm gives the explicit cubic-in-horizon logarithmic scale.

theorem telescopingHighProbabilityRegretLogBudget_standardExpectedRegretDelta {Feature : Type u} [Fintype Feature] (lambda : Real) (horizon : Nat) (L2 : Real) : telescopingHighProbabilityRegretLogBudget (Feature := Feature) lambda (standardExpectedRegretDelta horizon) horizon L2 = telescopingStandardExpectedRegretLogBudget (Feature := Feature) lambda horizon L2

Explicit expected pseudo-regret budget for a stopping time bounded by `T` under the single scheduled policy tuned with outer budget `1 / (T + 1)`.

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

The endpoint high-probability budget plus the tuned bad-event envelope charge is exactly the explicit scheduled expected pseudo-regret rate.

theorem telescopingHighProbabilityPseudoRegretBound_add_initial_standardExpectedRegretDelta_eq {Feature : Type u} [Fintype Feature] (R lambda S : Real) (horizon : Nat) (L2 : Real) : telescopingHighProbabilityPseudoRegretBound (Feature := Feature) R (standardExpectedRegretDelta horizon) lambda S horizon L2 + standardScalarInitialGapBound S L2 = telescopingStandardExpectedPseudoRegretBound (Feature := Feature) R lambda S horizon L2

Complete explicit expected pseudo-regret theorem for one bounded stopping time under the horizon-tuned telescoping-schedule OFUL policy.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_telescopingStandardExpectedBound_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) (S : Real) (hS : 0 <= S) (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) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K := K)) tau) (maxHorizon : Nat) (htau_le : forall trajectory, tau trajectory <= (maxHorizon : WithTop Nat)) : let delta := standardExpectedRegretDelta maxHorizon let mu := Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment let stoppedRegret := stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau 0 <= integral mu stoppedRegret /\ integral mu stoppedRegret <= telescopingStandardExpectedPseudoRegretBound (Feature := Feature) R lambda S maxHorizon L2

Expected stopped pseudo-regret for the horizon-indexed family of scheduled policies tuned at `delta_T = 1 / (T + 1)`.

noncomputable def canonicalTelescopingStandardExpectedStoppedPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (best : Fin K) (tau : Nat -> (Nat -> Fin K × Real) -> WithTop Nat) (maxHorizon : Nat) : Real

The named horizon-indexed expected stopped pseudo-regret is nonnegative and bounded pointwise by the explicit tuned scheduled rate.

theorem canonicalTelescopingStandardExpectedStoppedPseudoRegret_nonneg_and_le {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) (S : Real) (hS : 0 <= S) (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) (tau : Nat -> (Nat -> Fin K × Real) -> WithTop Nat) (htau : forall maxHorizon, IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K := K)) (tau maxHorizon)) (htau_le : forall maxHorizon trajectory, tau maxHorizon trajectory <= (maxHorizon : WithTop Nat)) (maxHorizon : Nat) : 0 <= canonicalTelescopingStandardExpectedStoppedPseudoRegret hK lambda thetaStar actionFeature R S environment best tau maxHorizon /\ canonicalTelescopingStandardExpectedStoppedPseudoRegret hK lambda thetaStar actionFeature R S environment best tau maxHorizon <= telescopingStandardExpectedPseudoRegretBound (Feature := Feature) R lambda S maxHorizon L2