BanditRLProof.OFULHighProbabilityRegretRate

The confidence logarithm for outer failure probability `delta` over the complete finite window `0, ..., horizon`.

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

At algorithm parameter `delta / (T+1)`, the standard confidence radius has the explicit form `R * sqrt (B_T + 2 * log ((T+1)/delta)) + sqrt lambda * S`.

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

Explicit complete finite-window high-probability pseudo-regret budget.

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

The named all-round gap budget is exactly the explicit rate expression.

theorem standardScalarAllRoundGapBound_eq_standardHighProbabilityPseudoRegretBound {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : standardScalarAllRoundGapBound (Feature := Feature) R delta lambda S horizon L2 = standardHighProbabilityPseudoRegretBound (Feature := Feature) R delta lambda S horizon L2

Complete fixed-optimal-arm pseudo-regret along one canonical trajectory.

noncomputable def canonicalStandardHighProbabilityPseudoRegret {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

Explicit finite-window high-probability pseudo-regret theorem for the canonical scalar-ridge OFUL trajectory. The horizon-`T` algorithm is run at `delta / (T+1)`. The result controls the complete rounds `0, ..., T`; it is not an anytime or all-horizon statement.

theorem canonicalStandardHighProbabilityPseudoRegret_nonneg_and_tail_le_explicitBound_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) (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 := delta / (((horizon + 1 : Nat) : Real)) let mu := Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment let pseudoRegret := canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon (forall trajectory, 0 <= pseudoRegret trajectory) /\ mu {trajectory | standardHighProbabilityPseudoRegretBound (Feature := Feature) R delta lambda S horizon L2 < pseudoRegret trajectory} <= ENNReal.ofReal delta