BanditRLProof.OFULScheduledCumulativeAlignedWindowPositiveCostBudgetExhaustionExpectedRegret

If accumulated resource reaches `budget` by `reachHorizon`, its first budget-exhaustion time is pointwise at most `reachHorizon`.

theorem budgetExhaustionTime_le_reachHorizon_of_spent_reach {Omega : Type v} (spent : Nat -> Omega -> Nat) (budget reachHorizon : Nat) (hreach : forall omega, budget <= spent reachHorizon omega) : forall omega, budgetExhaustionTime spent budget omega <= (reachHorizon : WithTop Nat)

An adapted budget-exhaustion time reached by an arbitrary deterministic horizon is square-integrable under every finite measure.

theorem squareIntegrableFiniteStoppingTime_budgetExhaustionTime_of_reachHorizon {Omega : Type v} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} (spent : Nat -> Omega -> Nat) (budget reachHorizon : Nat) (hspent : Adapted F spent) (hreach : forall omega, budget <= spent reachHorizon omega) : OFUL.SquareIntegrableFiniteStoppingTime mu (budgetExhaustionTime spent budget)

The round-count second moment of a budget-exhaustion time reached by `reachHorizon` is at most `(reachHorizon + 1)^2`.

theorem stoppingTimeRoundSecondMoment_budgetExhaustionTime_le_of_reachHorizon {Omega : Type v} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] {F : Filtration Nat mOmega} (spent : Nat -> Omega -> Nat) (budget reachHorizon : Nat) (hspent : Adapted F spent) (hreach : forall omega, budget <= spent reachHorizon omega) : let tau := budgetExhaustionTime spent budget let hstop := squareIntegrableFiniteStoppingTime_budgetExhaustionTime_of_reachHorizon mu spent budget reachHorizon hspent hreach OFUL.stoppingTimeRoundSecondMoment mu tau hstop <= (((reachHorizon + 1 : Nat) : Real)) ^ 2

Canonical scheduled OFUL expected pseudo-regret when budget exhaustion is known to occur by a separately supplied deterministic reach horizon.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_reachHorizonRoundsSq_add_initialGap_mul_reachHorizonRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_budgetExhaustionTime_reachedBy {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) (spent : Nat -> (Nat -> Fin K × Real) -> Nat) (budget reachHorizon : Nat) (hspent : Adapted (OFUL.canonicalHistoryTrajectoryAllRoundFiltration (K

If every aligned block of length `window` costs at least one, cumulative spend after `block * window` completed rounds is at least `block`.

theorem block_le_cumulativeSpent_mul_of_alignedWindowPositive {Omega : Type v} (cost : Nat -> Omega -> Nat) (window : Nat) (haligned : forall block omega, 1 <= (Finset.Ico (block * window) ((block + 1) * window)).sum (fun s => cost s omega)) : forall block omega, block <= cumulativeSpent cost (block * window) omega

Aligned-window positivity reaches resource threshold `budget` by completed round `budget * window`.

theorem budget_le_cumulativeSpent_budget_mul_of_alignedWindowPositive {Omega : Type v} (cost : Nat -> Omega -> Nat) (window budget : Nat) (haligned : forall block omega, 1 <= (Finset.Ico (block * window) ((block + 1) * window)).sum (fun s => cost s omega)) : forall omega, budget <= cumulativeSpent cost (budget * window) omega

Canonical scheduled OFUL expected pseudo-regret under aligned-window positive costs. Individual rounds may have zero cost; the deterministic reach horizon is `budget * window`.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetWindowRoundsSq_add_initialGap_mul_budgetWindowRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_cumulativeAlignedWindowPositiveCostBudgetExhaustionTime {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) (cost : Nat -> (Nat -> Fin K × Real) -> Nat) (window budget : Nat) (hcost : Adapted (OFUL.canonicalHistoryTrajectoryAllRoundFiltration (K