BanditRLProof.OFULScheduledBlockStartForcedHorizonWindowFiniteHorizonTail

A positive horizon used as its own block window has one forced successor index.

theorem blockStartForcedIndexSet_horizon_self_eq_singleton {horizon : Nat} (hhorizon : 0 < horizon) : blockStartForcedIndexSet horizon horizon = {0}

With `window = horizon > 0`, the forced successor charge is its first gap.

theorem blockStartForcedActionSuccessorPseudoRegret_horizon_self {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (forcedAction : Nat -> Fin K) {horizon : Nat} (hhorizon : 0 < horizon) : blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction horizon horizon = linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (forcedAction 0))

The exact horizon-window forced charge is bounded by one linear arm-gap envelope.

theorem blockStartForcedActionSuccessorPseudoRegret_horizon_self_le_two_mul_parameterFeatureBound {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S L2 : Real) (hS : 0 <= S) (htheta : euclideanLength thetaStar <= S) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (forcedAction : Nat -> Fin K) {horizon : Nat} (hhorizon : 0 < horizon) : blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction horizon horizon <= 2 * S * Real.sqrt L2

Fixed-horizon scalar violation event for the policy whose block window is that horizon.

noncomputable def blockStartForcedCanonicalStandardHighProbabilityPseudoRegretHorizonWindowViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (horizon : Nat) (best : Fin K) : Set (Nat -> Fin K × Real)

The one-charge fixed-horizon violation event is contained in the exact forced-charge all-horizon event for the same horizon-window policy.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegretHorizonWindowViolationSet_subset {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (hS : 0 <= S) (htheta : euclideanLength thetaStar <= S) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (forcedAction : Nat -> Fin K) {horizon : Nat} (hhorizon : 0 < horizon) (best : Fin K) : blockStartForcedCanonicalStandardHighProbabilityPseudoRegretHorizonWindowViolationSet lambda thetaStar actionFeature R delta S L2 horizon best ⊆ blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction horizon best

Fixed-horizon high-probability pseudo-regret theorem for the horizon-indexed block-start policy family. The forced charge is one linear arm-gap envelope.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegret_horizonWindow_nonneg_and_finiteHorizon_tail_le_explicitBound_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) (forcedAction : Nat -> Fin K) (horizon : Nat) (hhorizon : 0 < horizon) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : (forall trajectory, 0 <= canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) ∧ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction horizon) environment (blockStartForcedCanonicalStandardHighProbabilityPseudoRegretHorizonWindowViolationSet lambda thetaStar actionFeature R delta S L2 horizon best) <= ENNReal.ofReal delta