Lean module · OFUL
BanditRLProof.OFULScheduledBlockStartForcedPositiveActionCostBudgetExhaustionExpectedRegret
# Scheduled OFUL budget exhaustion from block-start forced positive actions The telescoping-confidence OFUL algorithm is deterministic conditional on its finite pair history. This module exposes its selected action as a named history function and transports the canonical successor-action law to an aligned-window positive-cost contract. At history index `block * window`, the policy generates trajectory action `block * window + 1`. Under `2 <= window`, that action lies in the aligned half-open block. If this selector is a fixed positive-cost `forcedAction block` for every history, the existing a.e. budget-reach theorem gives exhaustion by `budget * window` and closes the canonical expected-regret/tail terminal. The forced-selector equality is an explicit policy-design contract. Ordinary OFUL score maximization does not establish it, and this module does not modify the OFUL policy or claim a full bandits-with-knapsacks theorem.
Module map
Imports
BanditRLProof.OFULScheduledAEAlignedWindowPositiveActionCostBudgetExhaustionExpectedRegret
Imported by
BanditRLProof, BanditRLProof.OFULScheduledBlockStartForcedHistoryAlgorithm
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAction
Compiled
The action selected by the telescoping-confidence OFUL policy.
noncomputable def finiteHistoryTelescopingScalarRidgeOptimisticAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Fin K
theorem
BanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm_policy_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm_policy_apply {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S).policy n history = Measure.dirac (finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history)
theorem
BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryTelescopingScalarRidgeOptimisticAction
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryTelescopingScalarRidgeOptimisticAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, (trajectory (n + 1)).1 = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n (Preorder.frestrictLe n trajectory)
theorem
BanditRLProof.Budget.alignedWindowPositiveActionCostAE_of_blockStartTelescopingActionCostPositive
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem alignedWindowPositiveActionCostAE_of_blockStartTelescopingActionCostPositive {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (actionCost : Fin K -> Nat) (window : Nat) (hwindow : 2 <= window) (hpositive : forall block (history : History.FinitePairHistory (Fin K) Real (block * window)), 1 <= actionCost (OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S (block * window) history)) : AlignedWindowPositiveActionCostAE (Thompson.canonicalHistoryTrajectoryMeasure (OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) actionCost window
theorem
BanditRLProof.Budget.alignedWindowPositiveActionCostAE_of_blockStartForcedTelescopingAction
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem alignedWindowPositiveActionCostAE_of_blockStartForcedTelescopingAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (actionCost : Fin K -> Nat) (forcedAction : Nat -> Fin K) (window : Nat) (hwindow : 2 <= window) (hforced : forall block (history : History.FinitePairHistory (Fin K) Real (block * window)), OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S (block * window) history = forcedAction block) (hpositive : forall block, 1 <= actionCost (forcedAction block)) : AlignedWindowPositiveActionCostAE (Thompson.canonicalHistoryTrajectoryMeasure (OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) actionCost window
theorem
BanditRLProof.Budget.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetWindowRoundsSq_add_initialGap_mul_budgetWindowRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_blockStartForcedPositiveActionCostBudgetExhaustionTime
Compiled
Canonical scheduled OFUL expected pseudo-regret stopped at action-cost budget exhaustion when every aligned block contains a history-independent forced positive-cost action immediately after its block start.
theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetWindowRoundsSq_add_initialGap_mul_budgetWindowRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_blockStartForcedPositiveActionCostBudgetExhaustionTime {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) (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 : OFUL.IsOptimalLinearArm thetaStar actionFeature best) (source : OFUL.CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) (actionCost : Fin K -> Nat) (forcedAction : Nat -> Fin K) (window budget : Nat) (hwindow : 2 <= window) (hforced : forall block (history : History.FinitePairHistory (Fin K) Real (block * window)), OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S (block * window) history = forcedAction block) (hpositive : forall block, 1 <= actionCost (forcedAction block)) : let mu := Thompson.canonicalHistoryTrajectoryMeasure (OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment let tau := budgetExhaustionTime (cumulativeActionCost actionCost) budget let stoppedRegret := stoppedValue (fun horizon trajectory => OFUL.canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau let bad := OFUL.telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau 0 <= integral mu stoppedRegret /\ integral mu stoppedRegret <= OFUL.telescopingHighProbabilityPseudoRegretQuadraticCoefficient (Feature