BanditRLProof.OFULScheduledBlockStartForcedActionChargeBound

History indices whose successor action is prescribed by the block-start schedule.

def blockStartForcedIndexSet (window horizon : Nat) : Finset Nat

Every forced index below `horizon` belongs to the image of the quotient-block range under `block ↦ block * window`, so its cardinality is at most the number of quotient blocks. With `window = 0`, the modulo condition reduces to `n = 0`, and the same conservative bound remains valid.

theorem card_blockStartForcedIndexSet_le_div_add_one (window horizon : Nat) : (blockStartForcedIndexSet window horizon).card <= horizon / window + 1

A pointwise forced-arm gap ceiling bounds the forced charge by its cardinality.

theorem blockStartForcedActionSuccessorPseudoRegret_le_card_mul {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) (forcedGapBound : Real) (hforcedGap : forall block, linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (forcedAction block)) <= forcedGapBound) : blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon <= ((blockStartForcedIndexSet window horizon).card : Real) * forcedGapBound

The forced charge is at most the number of quotient blocks times a gap ceiling.

theorem blockStartForcedActionSuccessorPseudoRegret_le_div_add_one_mul {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) (forcedGapBound : Real) (hforcedGapBound : 0 <= forcedGapBound) (hforcedGap : forall block, linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (forcedAction block)) <= forcedGapBound) : blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon <= ((horizon / window + 1 : Nat) : Real) * forcedGapBound

Linear parameter and arm envelopes instantiate the generic forced-gap ceiling. No separate `0 <= L2` hypothesis is needed here: `Real.sqrt L2` is nonnegative, and the arm bound at `best` already rules out a negative feasible `L2`.

theorem blockStartForcedActionSuccessorPseudoRegret_le_div_add_one_mul_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) (window horizon : Nat) : blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon <= ((horizon / window + 1 : Nat) : Real) * (2 * S * Real.sqrt L2)

Fully scalar all-horizon violation event for the block-start forced policy.

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

The scalar-budget violation event is contained in the forced-charge event.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegretScalarAllHorizonViolationSet_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) (window : Nat) (best : Fin K) : blockStartForcedCanonicalStandardHighProbabilityPseudoRegretScalarAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 window best ⊆ blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction window best

Complete all-horizon theorem with the forced-action charge replaced by the scalar quotient-block count and the common linear arm-gap envelope.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_scalarAllHorizon_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) (window : Nat) (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 horizon trajectory, 0 <= canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) ∧ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment (blockStartForcedCanonicalStandardHighProbabilityPseudoRegretScalarAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 window best) <= ENNReal.ofReal delta