BanditRLProof.OFULScheduledBlockStartForcedPseudoRegretDecomposition

Away from block starts, the modified selector is the telescoping OFUL selector.

theorem finiteHistoryBlockStartForcedTelescopingScalarRidgeAction_eq_of_mod_ne_zero {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (window n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hnonforced : n % window ≠ 0) : finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window n history = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history

At a forced index, the modified selector is the prescribed block action.

theorem finiteHistoryBlockStartForcedTelescopingScalarRidgeAction_eq_forcedAction_of_mod_eq_zero {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (window n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hforced : n % window = 0) : finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window n history = forcedAction (n / window)

Under the modified policy's own trajectory law, every nonforced successor action agrees almost surely with the ordinary telescoping OFUL selector.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryTelescopingScalarRidgeOptimisticAction_of_mod_ne_zero {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (hnonforced : n % window ≠ 0) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, (trajectory (n + 1)).1 = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n (Preorder.frestrictLe n trajectory)

Successor pseudo-regret charged to block-start forced actions.

noncomputable def blockStartForcedSuccessorPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (window horizon : Nat) (trajectory : Nat -> Fin K × Real) : Real

Deterministic successor charge of the prescribed forced actions.

noncomputable def blockStartForcedActionSuccessorPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (forcedAction : Nat -> Fin K) (window horizon : Nat) : Real

Successor pseudo-regret charged to nonforced optimistic actions.

noncomputable def blockStartOptimisticSuccessorPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (window horizon : Nat) (trajectory : Nat -> Fin K × Real) : Real

Scheduled radius-width charge over the nonforced successor actions.

noncomputable def blockStartOptimisticSuccessorRadiusWidthCharge {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (window horizon : Nat) (trajectory : Nat -> Fin K × Real) : Real

Pathwise one-step optimism transport. The policy-specific input is only the equality between the observed successor action and the telescoping selector.

theorem canonicalHistoryTrajectory_action_succ_gap_le_of_eq_telescopingAction_of_not_mem_confidenceFailure {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) (trajectory : Nat -> Fin K × Real) (n : Nat) (comparator : Fin K) (haction : Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1) = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)) (hgood : trajectory ∉ scalarRidgeConfidenceFailureAt lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R (allTimeTelescopingDelta delta (n + 1)) (n + 1)) : linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1))) <= 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 complete pseudo-regret through action `horizon` is the initial gap plus the forced and nonforced successor charges. This identity is pathwise and does not require a probability or confidence assumption.

theorem canonicalStandardHighProbabilityPseudoRegret_eq_initial_add_blockStartForced_add_optimistic {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (window horizon : Nat) (trajectory : Nat -> Fin K × Real) : canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory = (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + blockStartForcedSuccessorPseudoRegret thetaStar actionFeature best window horizon trajectory + blockStartOptimisticSuccessorPseudoRegret thetaStar actionFeature best window horizon trajectory

Under the modified policy, the trajectory-valued forced successor charge is almost surely the deterministic charge of `forcedAction (n / window)`.

theorem blockStartForcedSuccessorPseudoRegret_ae_eq_forcedActionCharge {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : blockStartForcedSuccessorPseudoRegret thetaStar actionFeature best window horizon =ᵐ[ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment] fun _trajectory => blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon

On the all-time confidence event, the modified policy's nonforced successor pseudo-regret is bounded by its matching scheduled radius-width charge.

theorem blockStartOptimisticSuccessorPseudoRegret_le_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> blockStartOptimisticSuccessorPseudoRegret thetaStar actionFeature best window horizon trajectory <= blockStartOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S window horizon trajectory

Complete finite-horizon pseudo-regret bound for the modified policy on the all-time confidence event. Forced-round regret remains an explicit charge.

theorem canonicalStandardHighProbabilityPseudoRegret_le_initial_add_blockStartForced_add_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + blockStartForcedSuccessorPseudoRegret thetaStar actionFeature best window horizon trajectory + blockStartOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S window horizon trajectory

The modified-policy confidence-event bound with the forced successor charge written directly in terms of the prescribed forced actions.

theorem canonicalStandardHighProbabilityPseudoRegret_le_initial_add_forcedActionCharge_add_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon + blockStartOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S window horizon trajectory