BanditRLProof.OFULNormalizedRadiusWidth

No declaration docstring is present; use the chapter context and exact statement below.

theorem regularizedPrefixFeatureGram_inv_quadratic_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (feature : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) (hx : dotProduct x x <= lambda) : dotProduct x ((regularizedPrefixFeatureGram lambda feature T)⁻¹.mulVec x) <= 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem confidenceWidth_regularizedPrefixFeatureGram_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (feature : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) (hx : dotProduct x x <= lambda) : confidenceWidth (regularizedPrefixFeatureGram lambda feature T) x <= 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistoryTrajectory_confidenceWidth_le_one {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Fin K -> Feature -> Real) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (trajectory : Nat -> Fin K × Real) (t : Nat) : confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) t trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory t)) <= 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistoryTrajectory_sum_range_succ_radius_mul_width_le_standard_of_featureBound_le_regularization {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hdelta : 0 < delta) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (trajectory : Nat -> Fin K × Real) : (Finset.range horizon).sum (fun n => 2 * finiteHorizonScalarConfidenceRadius (canonicalHistoryTrajectoryFeature actionFeature) R (delta / ((horizon + 1 : Nat) : Real)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))) <= standardScalarRadiusWidthBound (Feature := Feature) R (delta / ((horizon + 1 : Nat) : Real)) lambda S (horizon + 1) L2

No declaration docstring is present; use the chapter context and exact statement below.

theorem measure_canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet_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 (canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator) <= ENNReal.ofReal delta