BanditRLProof.OFULExpectedRegretRate

The log budget in the horizon-tuned expected-regret radius: the standard log-determinant term plus the `4 * log (T+1)` confidence contribution.

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

The outer failure budget `1/(T+1)`, divided once more by the uniform-time schedule size, is exactly the algorithm parameter `1/(T+1)^2`.

theorem standardExpectedRegretAlgorithmDelta_eq_inv_sq (horizon : Nat) : standardExpectedRegretDelta horizon / (((horizon + 1 : Nat) : Real)) = 1 / (((horizon + 1 : Nat) : Real) ^ 2)

At the canonical horizon-tuned algorithm parameter, the standard confidence radius has the explicit form `R * sqrt (B_T + 4 * log (T+1)) + sqrt lambda * S`.

theorem standardScalarConfidenceRadiusUpper_standardExpectedRegret {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 < R) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : standardScalarConfidenceRadiusUpper (Feature := Feature) R (standardExpectedRegretDelta horizon / (((horizon + 1 : Nat) : Real))) lambda S (horizon + 1) L2 = R * Real.sqrt (standardExpectedRegretLogBudget (Feature := Feature) lambda horizon L2) + Real.sqrt lambda * S

Explicit logarithmic square-root bound for expected OFUL pseudo-regret.

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

The prior named expected bound is exactly the explicit rate expression.

theorem standardScalarAllRoundGapBound_add_initial_eq_standardExpectedPseudoRegretBound {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 < R) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : standardScalarAllRoundGapBound (Feature := Feature) R (standardExpectedRegretDelta horizon) lambda S horizon L2 + standardScalarInitialGapBound S L2 = standardExpectedPseudoRegretBound (Feature := Feature) R lambda S horizon L2

Explicit finite-window expected pseudo-regret theorem for the canonical scalar-ridge OFUL trajectory. The algorithm parameter is displayed directly as `1/(T+1)^2`, and the upper bound is the logarithmic square-root expression `standardExpectedPseudoRegretBound`.

theorem integral_canonicalHistoryTrajectoryPseudoRegret_nonneg_and_le_explicitStandardExpectedBound_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) (horizon : Nat) (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) : let algorithmDelta := 1 / (((horizon + 1 : Nat) : Real) ^ 2) let expectedPseudoRegret := integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment) (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon (fun _t => best)) 0 <= expectedPseudoRegret ∧ expectedPseudoRegret <= standardExpectedPseudoRegretBound (Feature := Feature) R lambda S horizon L2