BanditRLProof.OFULScheduledAllHorizonHighProbabilityRegretRate

The explicit confidence logarithm induced at horizon `T` by the telescoping failure share `delta / ((T+1)(T+2))`.

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

Explicit complete all-round pseudo-regret budget for the telescoping-schedule policy at a finite horizon.

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

The time-`T` telescoping share is a finite-window confidence parameter with outer budget `delta / (T+2)`.

theorem allTimeTelescopingDelta_eq_outerBudget_div_succ (delta : Real) (horizon : Nat) : allTimeTelescopingDelta delta horizon = (delta / (((horizon + 2 : Nat) : Real))) / (((horizon + 1 : Nat) : Real))

The finite-window confidence logarithm at outer budget `delta / (T+2)` is the explicit telescoping confidence logarithm.

theorem standardHighProbabilityRegretLogBudget_outerBudget_eq_telescoping {Feature : Type u} [Fintype Feature] (lambda delta : Real) (hdelta : 0 < delta) (horizon : Nat) (L2 : Real) : standardHighProbabilityRegretLogBudget (Feature

The finite-window explicit pseudo-regret budget at outer confidence `delta / (T+2)` is exactly the explicit telescoping budget.

theorem standardHighProbabilityPseudoRegretBound_outerBudget_eq_telescoping {Feature : Type u} [Fintype Feature] (R delta lambda S : Real) (hdelta : 0 < delta) (horizon : Nat) (L2 : Real) : standardHighProbabilityPseudoRegretBound (Feature

The named scheduled all-round budget is exactly the explicit telescoping pseudo-regret rate at every finite horizon.

theorem telescopingStandardScalarAllRoundGapBound_eq_telescopingHighProbabilityPseudoRegretBound {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) : telescopingStandardScalarAllRoundGapBound (Feature

Explicit all-horizon violation event for the named fixed-best pseudo-regret under the one telescoping-schedule policy.

noncomputable def telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet {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 -> Prod (Fin K) Real)

The explicit violation event is the compiled abstract scheduled violation event.

theorem telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet_eq_standard {K : Nat} {Feature : Type u} [Fintype Feature] [Nonempty Feature] (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 L2 : Real) (hL2 : 0 <= L2) (best : Fin K) : telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best = telescopingCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best

Complete explicit one-policy all-horizon high-probability pseudo-regret theorem for telescoping-schedule OFUL.

theorem telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_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) (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) : (forall horizon trajectory, 0 <= canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) /\ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best) <= ENNReal.ofReal delta