BanditRLProof.OFULGeneratedTrajectoryConfidenceGap

Any action whose optimistic score dominates a comparator satisfies the usual two-bonus OFUL gap bound on the confidence ellipsoid.

theorem linearValue_sub_selected_le_two_mul_bonus_of_score_max {Feature Action : Type*} [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (thetaHat thetaStar : Feature -> Real) (beta : Real) (actionFeature : Action -> Feature -> Real) (selected comparator : Action) (hconfidence : matrixNorm V (thetaHat - thetaStar) <= beta) (hscoreMax : optimisticScore thetaHat V beta (actionFeature comparator) <= optimisticScore thetaHat V beta (actionFeature selected)) : linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature selected) <= 2 * beta * confidenceWidth V (actionFeature selected)

The concrete strict-fold history selector has the OFUL one-step gap certificate. No identification with the nonconstructive finite argmax is used.

theorem finiteHistoryScalarRidgeOptimisticAction_gap_le {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hconfidence : matrixNorm (finiteHistoryScalarRidgeDesign lambda actionFeature n history) (finiteHistoryScalarRidgeEstimate lambda actionFeature n history - thetaStar) <= finiteHistoryScalarRidgeRadius actionFeature R delta lambda S n history) (comparator : Fin K) : linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (finiteHistoryScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history)) <= 2 * finiteHistoryScalarRidgeRadius actionFeature R delta lambda S n history * confidenceWidth (finiteHistoryScalarRidgeDesign lambda actionFeature n history) (actionFeature (finiteHistoryScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history))

Feature process obtained by projecting actions from a canonical trajectory.

def canonicalHistoryTrajectoryFeature {K : Nat} {Feature : Type u} (actionFeature : Fin K -> Feature -> Real) (t : Nat) (trajectory : (k : Nat) -> Fin K × Real) : Feature -> Real

Response process obtained by projecting rewards from a canonical trajectory.

def canonicalHistoryTrajectoryResponse {K : Nat} (t : Nat) (trajectory : (k : Nat) -> Fin K × Real) : Real

A trace prefix exposes the original action feature at every stored index.

@[simp] theorem finiteHistoryObservedFeature_finitePairHistoryOfTrace_of_le {K : Nat} {Feature : Type u} (actionFeature : Fin K -> Feature -> Real) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n t : Nat) (ht : t <= n) : finiteHistoryObservedFeature actionFeature n (History.finitePairHistoryOfTrace action reward n) t = actionFeature (action t)

A trace prefix exposes the original response at every stored index.

@[simp] theorem finiteHistoryObservedResponse_finitePairHistoryOfTrace_of_le {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n t : Nat) (ht : t <= n) : finiteHistoryObservedResponse n (History.finitePairHistoryOfTrace action reward n) t = reward t

The feature Gram reconstructed from inclusive history `n` is exactly the trajectory feature Gram at horizon `n + 1`.

theorem finiteHorizonFeatureGram_finitePairHistoryOfTrace_eq {K : Nat} {Feature : Type u} [Fintype Feature] (actionFeature : Fin K -> Feature -> Real) (trajectory : (k : Nat) -> Fin K × Real) (n : Nat) : finiteHorizonFeatureGram (fun t historyValue => finiteHistoryObservedFeature actionFeature n historyValue t) (n + 1) (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) = finiteHorizonFeatureGram (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory

The response vector reconstructed from inclusive history `n` is exactly the trajectory response vector at horizon `n + 1`.

theorem finiteHorizonResponseVector_finitePairHistoryOfTrace_eq {K : Nat} {Feature : Type u} [Fintype Feature] (actionFeature : Fin K -> Feature -> Real) (trajectory : (k : Nat) -> Fin K × Real) (n : Nat) : finiteHorizonResponseVector (fun t historyValue => finiteHistoryObservedFeature actionFeature n historyValue t) (fun t historyValue => finiteHistoryObservedResponse n historyValue t) (n + 1) (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) = finiteHorizonResponseVector (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse (n + 1) trajectory

Exact design-matrix alignment between finite history and trajectory state.

theorem finiteHistoryScalarRidgeDesign_finitePairHistoryOfTrace_eq {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (trajectory : (k : Nat) -> Fin K × Real) (n : Nat) : finiteHistoryScalarRidgeDesign lambda actionFeature n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) = finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory

Exact ridge-estimate alignment between finite history and trajectory state.

theorem finiteHistoryScalarRidgeEstimate_finitePairHistoryOfTrace_eq {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (trajectory : (k : Nat) -> Fin K × Real) (n : Nat) : finiteHistoryScalarRidgeEstimate lambda actionFeature n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) = finiteHorizonRidgeEstimate (Matrix.scalar Feature lambda) (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse (n + 1) trajectory

Exact confidence-radius alignment between finite history and trajectory.

theorem finiteHistoryScalarRidgeRadius_finitePairHistoryOfTrace_eq {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (trajectory : (k : Nat) -> Fin K × Real) (n : Nat) : finiteHistoryScalarRidgeRadius actionFeature R delta lambda S n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) = finiteHorizonScalarConfidenceRadius (canonicalHistoryTrajectoryFeature actionFeature) R delta lambda S (n + 1) trajectory

Outside the generic fixed-time confidence failure set, the actual canonical successor action satisfies the concrete OFUL one-step gap certificate.

theorem canonicalHistoryTrajectory_action_succ_gap_le_of_not_mem_confidenceFailure {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) (n : Nat) (comparator : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∉ scalarRidgeConfidenceFailureAt lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta (n + 1) -> linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1))) <= 2 * finiteHorizonScalarConfidenceRadius (canonicalHistoryTrajectoryFeature actionFeature) R delta lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))

On the equal-share uniform confidence event, all canonical successor rounds `1, ..., horizon` satisfy the cumulative OFUL bonus bound. The fixed initial round `0` is not part of this sum.

theorem canonicalHistoryTrajectory_sum_range_succ_gap_le_on_uniformConfidence {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 (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment, trajectory ∉ finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta horizon -> (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 (delta / ((horizon + 1 : Nat) : Real)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1))))