BanditRLProof.OFULGeneratedTrajectoryRadiusWidth

The standard log-determinant budget for a bounded scalar-ridge prefix.

noncomputable def standardScalarLogDetBudget {Feature : Type u} [Fintype Feature] (lambda : Real) (T : Nat) (L2 : Real) : Real

A deterministic upper radius obtained by replacing the random determinant ratio with `exp (standardScalarLogDetBudget ...)`.

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

The selected-width budget paired with the standard log-determinant term.

noncomputable def standardSelectedWidthBudget {Feature : Type u} [Fintype Feature] (lambda : Real) (T : Nat) (L2 : Real) : Real

Deterministic radius-times-width budget used by the canonical gap theorem.

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

The process scalar Gram is definitionally the regularized feature prefix.

theorem finiteHorizonScalarGram_eq_regularizedPrefixFeatureGram {Omega Feature : Type*} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : finiteHorizonScalarGram lambda feature n omega = regularizedPrefixFeatureGram lambda (fun t => feature t omega) n

The standard log-determinant budget is monotone in the horizon.

theorem standardScalarLogDetBudget_mono {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (L2 : Real) (hL2 : 0 <= L2) {n T : Nat} (hnT : n <= T) : standardScalarLogDetBudget (Feature := Feature) lambda n L2 <= standardScalarLogDetBudget (Feature := Feature) lambda T L2

The standard log-determinant budget is nonnegative.

theorem standardScalarLogDetBudget_nonneg {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) : 0 <= standardScalarLogDetBudget (Feature := Feature) lambda T L2

Every prefix scalar confidence radius is bounded by the standard deterministic radius at a later horizon.

theorem finiteHorizonScalarConfidenceRadius_le_standardUpper {Omega Feature : Type*} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (feature : Nat -> Omega -> Feature -> Real) (R delta S : Real) (omega : Omega) (n T : Nat) (hnT : n <= T) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (feature t omega) (feature t omega) <= L2) (hdelta : 0 < delta) : finiteHorizonScalarConfidenceRadius feature R delta lambda S n omega <= standardScalarConfidenceRadiusUpper (Feature := Feature) R delta lambda S T L2

The standard deterministic confidence-radius upper bound is nonnegative.

theorem standardScalarConfidenceRadiusUpper_nonneg {Feature : Type u} [Fintype Feature] (R delta lambda S : Real) (T : Nat) (L2 : Real) (hS : 0 <= S) : 0 <= standardScalarConfidenceRadiusUpper (Feature := Feature) R delta lambda S T L2

The standard selected-width budget is nonnegative.

theorem standardSelectedWidthBudget_nonneg {Feature : Type u} [Fintype Feature] (lambda : Real) (T : Nat) (L2 : Real) : 0 <= standardSelectedWidthBudget (Feature := Feature) lambda T L2

Pointwise canonical successor bonus bound. The full action prefix through `horizon` is charged to the selected-width theorem, while the gap sum only uses successor rounds `1, ..., horizon`.

theorem canonicalHistoryTrajectory_sum_range_succ_radius_mul_width_le_standard {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) (trajectory : Nat -> Fin K × Real) (hwidth : forall t, t < horizon + 1 -> confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) t trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory t)) <= 1) : (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

Violation of the deterministic standard radius-times-width successor-gap budget. The fixed initial gap is still excluded.

def canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet {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)

The deterministic-budget violation event is contained in the compiled random radius-times-width violation event.

theorem canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet_subset {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (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) (comparator : Nat -> Fin K) (hwidth : forall trajectory t, t < horizon + 1 -> confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) t trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory t)) <= 1) : canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator <= canonicalHistoryTrajectorySumRangeSuccGapViolationSet lambda thetaStar actionFeature R delta S horizon comparator

Concrete high-probability successor-gap theorem with a deterministic standard radius-times-width budget under the linear-sub-Gaussian environment law.

theorem measure_canonicalHistoryTrajectorySumRangeSuccGapStandardViolationSet_le_of_linearSubgaussianEnvironment {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) (comparator : Nat -> Fin K) (hwidth : forall trajectory t, t < horizon + 1 -> confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) t trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory t)) <= 1) (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