Lean module · OFUL
BanditRLProof.OFULNormalizedRadiusWidth
# Normalized scalar-ridge OFUL confidence widths This module derives the raw `confidenceWidth <= 1` contract from the explicit normalization `dotProduct x x <= L2 <= lambda`, then exposes the canonical standard successor-gap tail without a caller-supplied width premise.
Module map
Imports
BanditRLProof.OFULGeneratedTrajectoryRadiusWidth
Imported by
BanditRLProof, BanditRLProof.OFULInitialRoundGap, BanditRLProof.OFULScheduledAllHorizonCumulativeGap
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.regularizedPrefixFeatureGram_inv_quadratic_le_one
Compiled
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
theorem
BanditRLProof.OFUL.confidenceWidth_regularizedPrefixFeatureGram_le_one
Compiled
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
theorem
BanditRLProof.OFUL.canonicalHistoryTrajectory_confidenceWidth_le_one
Compiled
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
theorem
BanditRLProof.OFUL.canonicalHistoryTrajectory_sum_range_succ_radius_mul_width_le_standard_of_featureBound_le_regularization
Compiled
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
theorem
BanditRLProof.OFUL.measure_canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet_le_of_linearSubgaussianEnvironment_of_featureBound_le_regularization
Compiled
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