BanditRLProof.OFULScheduledBudgetExhaustionExpectedRegret

A stopping time bounded by a deterministic natural horizon has the local square-integrable finite-stopping contract under any finite measure.

theorem squareIntegrableFiniteStoppingTime_of_bounded {Omega : Type v} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} (tau : Omega -> WithTop Nat) (htau : IsStoppingTime F tau) (bound : Nat) (htau_le : forall omega, tau omega <= (bound : WithTop Nat)) : SquareIntegrableFiniteStoppingTime mu tau

The exact second moment of a deterministically bounded square-integrable stopping time is at most the square of the corresponding round-count bound.

theorem stoppingTimeRoundSecondMoment_le_sq_of_bounded {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (tau : Omega -> WithTop Nat) (hstop : SquareIntegrableFiniteStoppingTime mu tau) (bound : Nat) (htau_le : forall omega, tau omega <= (bound : WithTop Nat)) : stoppingTimeRoundSecondMoment mu tau hstop <= (((bound + 1 : Nat) : Real)) ^ 2

If the accumulated resource has reached `budget` by index `budget`, its first budget-exhaustion time is pointwise at most `budget`.

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

An adapted budget-exhaustion time reached by index `budget` is a square-integrable finite stopping time under every finite measure.

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

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

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

Canonical expected pseudo-regret bound for the single telescoping-schedule OFUL policy stopped at a reached-by-budget resource exhaustion time.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetRoundsSq_add_initialGap_mul_budgetRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_budgetExhaustionTime {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 : Nat) (hspent : Adapted (OFUL.canonicalHistoryTrajectoryAllRoundFiltration (K