BanditRLProof.OFULGeneratedTrajectoryUniformConfidence

Regularity source needed to apply scalar-ridge uniform confidence to one canonical history-algorithm trajectory. The selected feature is the actual canonical action feature. Constructing this source from a concrete reward environment therefore remains a genuine predictability and conditional-law obligation.

structure CanonicalScalarRidgeConfidenceSource {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (horizon : Nat) where

The generic equal-share scalar-ridge confidence theorem specialized to one canonical history-algorithm trajectory.

theorem measure_canonicalHistoryTrajectory_uniformScalarRidgeConfidenceFailureSet_le {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (S : Real) (horizon : Nat) (source : CanonicalScalarRidgeConfidenceSource algorithm environment thetaStar actionFeature R S horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) : Thompson.canonicalHistoryTrajectoryMeasure algorithm environment (finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta horizon) <= ENNReal.ofReal delta

Strict violation of the compiled successor-window OFUL good-event gap bound. The range index `n` is charged to the actual action at time `n + 1`, so time zero is not part of this event.

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

Canonical high-probability successor-gap theorem. Under the exact generated feature/noise/response regularity source, the probability that the cumulative true linear gap over rounds `1, ..., horizon` exceeds the compiled radius-times-width sum is at most the total confidence budget `delta`.

theorem measure_canonicalHistoryTrajectorySumRangeSuccGapViolationSet_le {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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (comparator : Nat -> Fin K) (source : CanonicalScalarRidgeConfidenceSource (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment thetaStar actionFeature R S horizon) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment (canonicalHistoryTrajectorySumRangeSuccGapViolationSet lambda thetaStar actionFeature R delta S horizon comparator) <= ENNReal.ofReal delta