BanditRLProof.OFULScheduledAllHorizonAllRoundGap

Scheduled deterministic cumulative-gap budget including time zero.

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

The time-zero gap envelope holds on the trajectory generated by the single telescoping-schedule policy.

theorem telescopingCanonicalHistoryTrajectory_initialGap_le_ae {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hS : 0 <= S) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (environment : Thompson.HistoryEnvironment (Fin K) Real) (comparator : Fin K) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0)) <= standardScalarInitialGapBound S L2

There exists a finite horizon whose complete gap over rounds `0, ..., horizon` exceeds the corresponding scheduled initial-plus-radius-width budget.

noncomputable def telescopingCanonicalHistoryTrajectoryAllHorizonAllRoundGapStandardViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (comparator : Nat -> Fin K) : Set (Nat -> Fin K × Real)

Almost surely, every all-round all-horizon violation gives a successor-only all-horizon violation at the same witness horizon.

theorem telescopingCanonicalHistoryTrajectoryAllHorizonAllRoundGapStandardViolationSet_subset_succ_ae {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (comparator : Nat -> Fin K) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∈ telescopingCanonicalHistoryTrajectoryAllHorizonAllRoundGapStandardViolationSet lambda thetaStar actionFeature R delta S L2 comparator -> trajectory ∈ telescopingCanonicalHistoryTrajectoryAllHorizonSuccGapStandardViolationSet lambda thetaStar actionFeature R delta S L2 comparator

The probability of any finite-horizon complete cumulative-gap violation for the one telescoping-schedule policy is at most `delta`.

theorem measure_telescopingCanonicalHistoryTrajectoryAllHorizonAllRoundGapStandardViolationSet_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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (comparator : Nat -> Fin K) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalHistoryTrajectoryAllHorizonAllRoundGapStandardViolationSet lambda thetaStar actionFeature R delta S L2 comparator) <= ENNReal.ofReal delta

All-horizon violation event for the named fixed-best pseudo-regret.

noncomputable def telescopingCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet {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)

Complete one-policy all-horizon high-probability pseudo-regret theorem. The fixed-best pseudo-regret is nonnegative at every finite horizon, and the probability that any horizon exceeds its scheduled standard budget is at most `delta`.

theorem telescopingCanonicalStandardHighProbabilityPseudoRegret_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) (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 (telescopingCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best) <= ENNReal.ofReal delta