BanditRLProof.OFULScheduledAllHorizonCumulativeGap

The telescoping confidence schedule is antitone in its time index.

theorem allTimeTelescopingDelta_antitone {delta : Real} (hdelta : 0 <= delta) {n T : Nat} (hnT : n <= T) : allTimeTelescopingDelta delta T <= allTimeTelescopingDelta delta n

For fixed determinant budget, the standard confidence-radius upper bound is antitone in the positive confidence level.

theorem standardScalarConfidenceRadiusUpper_antitone_delta {Feature : Type u} [Fintype Feature] (R lambda S : Real) (T : Nat) (L2 : Real) {deltaSmall deltaLarge : Real} (hdeltaSmall : 0 < deltaSmall) (hdelta : deltaSmall <= deltaLarge) : standardScalarConfidenceRadiusUpper (Feature := Feature) R deltaLarge lambda S T L2 <= standardScalarConfidenceRadiusUpper (Feature := Feature) R deltaSmall lambda S T L2

Every prefix radius using the varying telescoping schedule is bounded by one standard radius using separate terminal schedule and Gram-matrix budgets.

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

Every prefix radius using the varying telescoping schedule is bounded by one standard radius using the same terminal index for both budgets.

theorem finiteHorizonScalarConfidenceRadius_telescoping_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) (hdelta : 0 < delta) (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) : finiteHorizonScalarConfidenceRadius feature R (allTimeTelescopingDelta delta n) lambda S n omega <= standardScalarConfidenceRadiusUpper (Feature := Feature) R (allTimeTelescopingDelta delta T) lambda S T L2

Standard varying-budget radius-width envelope at a finite horizon.

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

The scheduled successor bonuses up to a fixed horizon obey one deterministic terminal radius-times-width budget.

theorem canonicalHistoryTrajectory_sum_range_succ_telescoping_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 (allTimeTelescopingDelta delta (n + 1)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))) <= telescopingStandardScalarRadiusWidthBound (Feature := Feature) R delta lambda S horizon L2

The explicit feature normalization `L2 <= lambda` discharges every scheduled selected-width premise.

theorem canonicalHistoryTrajectory_sum_range_succ_telescoping_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 (allTimeTelescopingDelta delta (n + 1)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))) <= telescopingStandardScalarRadiusWidthBound (Feature := Feature) R delta lambda S horizon L2

Outside the single all-time confidence failure event, every fixed-horizon successor-gap sum is bounded by its scheduled radius-times-width sum.

theorem telescopingCanonicalHistoryTrajectory_sum_range_succ_gap_le_radius_mul_width_ae {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 delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (comparator : Nat -> Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> (Finset.range horizon).sum (fun n => linearValue thetaStar (actionFeature (comparator (n + 1))) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))) <= (Finset.range horizon).sum (fun n => 2 * finiteHorizonScalarConfidenceRadius (canonicalHistoryTrajectoryFeature actionFeature) R (allTimeTelescopingDelta delta (n + 1)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1))))

The normalized feature contract turns the scheduled fixed-horizon gap sum into the deterministic terminal standard budget on the same all-time good event.

theorem telescopingCanonicalHistoryTrajectory_sum_range_succ_gap_le_standard_ae_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 delta S : Real) (hdelta : 0 < delta) (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) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> (Finset.range horizon).sum (fun n => linearValue thetaStar (actionFeature (comparator (n + 1))) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))) <= telescopingStandardScalarRadiusWidthBound (Feature := Feature) R delta lambda S horizon L2

There exists a finite horizon whose cumulative successor gap exceeds the corresponding scheduled deterministic terminal budget.

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

Any all-horizon cumulative successor-gap violation forces the one-policy all-time confidence failure event almost surely.

theorem telescopingCanonicalHistoryTrajectoryAllHorizonSuccGapStandardViolationSet_subset_confidenceFailure_ae {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 delta S : Real) (hdelta : 0 < delta) (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) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∈ telescopingCanonicalHistoryTrajectoryAllHorizonSuccGapStandardViolationSet lambda thetaStar actionFeature R delta S L2 comparator -> trajectory ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta

For the one telescoping-schedule generated policy, the probability that any finite-horizon cumulative successor gap exceeds its scheduled deterministic standard budget is at most `delta`.

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