BanditRLProof.OFULInitialRoundGap

Ordinary finite-dimensional Cauchy--Schwarz on the local linear-value surface.

theorem abs_linearValue_le_euclideanLength_mul_euclideanLength {Feature : Type u} [Fintype Feature] (theta x : Feature -> Real) : |linearValue theta x| <= euclideanLength theta * euclideanLength x

A common parameter/feature envelope bounds the absolute linear value.

theorem abs_linearValue_le_parameterFeatureBound {Feature : Type u} [Fintype Feature] (theta x : Feature -> Real) (S L2 : Real) (hS : 0 <= S) (htheta : euclideanLength theta <= S) (hx : dotProduct x x <= L2) : |linearValue theta x| <= S * Real.sqrt L2

Two arms sharing the same feature envelope differ by at most `2*S*sqrt L2`.

theorem linearValue_sub_linearValue_le_two_mul_parameterFeatureBound {Feature : Type u} [Fintype Feature] (theta x y : Feature -> Real) (S L2 : Real) (hS : 0 <= S) (htheta : euclideanLength theta <= S) (hx : dotProduct x x <= L2) (hy : dotProduct y y <= L2) : linearValue theta x - linearValue theta y <= 2 * S * Real.sqrt L2

Deterministic charge used for the canonical time-zero arm.

noncomputable def standardScalarInitialGapBound (S L2 : Real) : Real

The canonical OFUL initial action is the fixed arm `0` almost surely, so its linear gap to any comparator is bounded by the common parameter/feature envelope.

theorem canonicalHistoryTrajectory_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 algorithmDelta 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 (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment, linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0)) <= standardScalarInitialGapBound S L2

Standard finite-window cumulative-gap budget including time zero.

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

Violation of the standard OFUL cumulative-gap budget over rounds `0, ..., horizon`.

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

Almost surely, an all-round violation implies the previously compiled successor-only standard-budget violation.

theorem canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet_ae_le_succ {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) (horizon : Nat) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (comparator : Nat -> Fin K) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment, trajectory ∈ canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator -> trajectory ∈ canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator

Concrete high-probability standard cumulative-gap theorem over all rounds `0, ..., horizon`, with automatic normalized width discharge.

theorem measure_canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet_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) (horizon : Nat) (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 (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment (canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator) <= ENNReal.ofReal delta