Lean module · OFUL
BanditRLProof.OFULScheduledCumulativePositiveCostBudgetExhaustionExpectedRegret
# Scheduled OFUL expected regret under cumulative positive costs This module constructs an adapted Nat-valued resource process by summing per-round costs over completed rounds. Pointwise positive costs give the unit-growth contract required by the compiled budget-exhaustion OFUL theorem.
Module map
Imports
BanditRLProof.OFULScheduledUnitGrowthBudgetExhaustionExpectedRegret
Imported by
BanditRLProof, BanditRLProof.OFULScheduledCumulativeAlignedWindowPositiveCostBudgetExhaustionExpectedRegret, BanditRLProof.OFULScheduledPositiveActionCostBudgetExhaustionExpectedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Budget.cumulativeSpent
Compiled
Resource spent after `t` completed rounds, using the half-open index set `{0, ..., t - 1}`.
def cumulativeSpent {Omega : Type v} (cost : Nat -> Omega -> Nat) (t : Nat) (omega : Omega) : Nat
theorem
BanditRLProof.Budget.cumulativeSpent_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem cumulativeSpent_zero {Omega : Type v} (cost : Nat -> Omega -> Nat) (omega : Omega) : cumulativeSpent cost 0 omega = 0
theorem
BanditRLProof.Budget.cumulativeSpent_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem cumulativeSpent_succ {Omega : Type v} (cost : Nat -> Omega -> Nat) (t : Nat) (omega : Omega) : cumulativeSpent cost (t + 1) omega = cumulativeSpent cost t omega + cost t omega
theorem
BanditRLProof.Budget.adapted_cumulativeSpent
Compiled
Finite prefix sums of an adapted per-round Nat-valued cost process remain adapted. A cost observed at `s < t` is promoted from `F s` to `F t`.
theorem adapted_cumulativeSpent {Omega : Type v} [mOmega : MeasurableSpace Omega] {F : Filtration Nat mOmega} {cost : Nat -> Omega -> Nat} (hcost : Adapted F cost) : Adapted F (cumulativeSpent cost)
theorem
BanditRLProof.Budget.cumulativeSpent_unitGrowth_of_one_le
Compiled
If every completed round costs at least one, cumulative spend grows by at least one at each step.
theorem cumulativeSpent_unitGrowth_of_one_le {Omega : Type v} (cost : Nat -> Omega -> Nat) (hcost : forall t omega, 1 <= cost t omega) : forall t omega, cumulativeSpent cost t omega + 1 <= cumulativeSpent cost (t + 1) omega
theorem
BanditRLProof.Budget.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetRoundsSq_add_initialGap_mul_budgetRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_cumulativePositiveCostBudgetExhaustionTime
Compiled
Canonical expected pseudo-regret bound for the single telescoping-schedule OFUL policy stopped when the cumulative positive per-round cost reaches the budget.
theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetRoundsSq_add_initialGap_mul_budgetRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_cumulativePositiveCostBudgetExhaustionTime {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) (budget : Nat) (hcost : Adapted (OFUL.canonicalHistoryTrajectoryAllRoundFiltration (K