BanditRLProof.OFULScheduledAEAlignedWindowPositiveActionCostBudgetExhaustionExpectedRegret

An almost-everywhere deterministic bound supplies the local square-integrable finite-stopping contract. Values outside the support may remain unbounded.

theorem squareIntegrableFiniteStoppingTime_of_bounded_ae {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 : ∀ᵐ omega ∂mu, tau omega <= (bound : WithTop Nat)) : SquareIntegrableFiniteStoppingTime mu tau

The exact round-count second moment obeys the same numerical square bound when the stopping-time bound is only almost everywhere.

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

Almost-everywhere resource reach gives an almost-everywhere deterministic bound on the first budget-exhaustion time.

theorem budgetExhaustionTime_le_reachHorizon_ae_of_spent_reach {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) (spent : Nat -> Omega -> Nat) (budget reachHorizon : Nat) (hreach : ∀ᵐ omega ∂mu, budget <= spent reachHorizon omega) : ∀ᵐ omega ∂mu, budgetExhaustionTime spent budget omega <= (reachHorizon : WithTop Nat)

An adapted budget-exhaustion time reached almost surely by a deterministic horizon is square-integrable under every finite measure.

theorem squareIntegrableFiniteStoppingTime_budgetExhaustionTime_of_reachHorizon_ae {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 : ∀ᵐ omega ∂mu, budget <= spent reachHorizon omega) : OFUL.SquareIntegrableFiniteStoppingTime mu (budgetExhaustionTime spent budget)

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

theorem stoppingTimeRoundSecondMoment_budgetExhaustionTime_le_of_reachHorizon_ae {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 : ∀ᵐ omega ∂mu, budget <= spent reachHorizon omega) : let tau := budgetExhaustionTime spent budget let hstop := squareIntegrableFiniteStoppingTime_budgetExhaustionTime_of_reachHorizon_ae 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 occurs by a deterministic reach horizon almost surely under the canonical measure.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_reachHorizonRoundsSq_add_initialGap_mul_reachHorizonRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_budgetExhaustionTime_reachedBy_ae {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

Almost every trajectory selects an action with positive deterministic cost at least once in every aligned half-open block.

def AlignedWindowPositiveActionCostAE {K : Nat} (mu : Measure (Nat -> Fin K × Real)) (actionCost : Fin K -> Nat) (window : Nat) : Prop

The all-block a.e. contract is equivalent to proving the selected positive-cost witness almost surely for each natural block separately.

theorem alignedWindowPositiveActionCostAE_iff_forall_ae {K : Nat} (mu : Measure (Nat -> Fin K × Real)) (actionCost : Fin K -> Nat) (window : Nat) : AlignedWindowPositiveActionCostAE mu actionCost window ↔ forall block, ∀ᵐ trajectory ∂mu, exists s, s ∈ Finset.Ico (block * window) ((block + 1) * window) /\ 1 <= actionCost (trajectory s).1

One positive selected-action cost in each aligned block makes the whole block sum positive almost surely.

theorem canonicalActionCostProcess_alignedWindowPositive_ae {K : Nat} (mu : Measure (Nat -> Fin K × Real)) (actionCost : Fin K -> Nat) (window : Nat) (hwindow : AlignedWindowPositiveActionCostAE mu actionCost window) : ∀ᵐ trajectory ∂mu, forall block, 1 <= (Finset.Ico (block * window) ((block + 1) * window)).sum (fun s => canonicalActionCostProcess actionCost s trajectory)

The a.e. aligned selected-action contract reaches cumulative action-cost budget by completed round `budget * window`.

theorem budget_le_cumulativeActionCost_budget_mul_ae {K : Nat} (mu : Measure (Nat -> Fin K × Real)) (actionCost : Fin K -> Nat) (window budget : Nat) (hwindow : AlignedWindowPositiveActionCostAE mu actionCost window) : ∀ᵐ trajectory ∂mu, budget <= cumulativeActionCost actionCost (budget * window) trajectory

Canonical scheduled OFUL expected pseudo-regret stopped at deterministic selected-action cost budget exhaustion under an a.e. aligned-window positive cost contract.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_budgetWindowRoundsSq_add_initialGap_mul_budgetWindowRounds_mul_sqrt_delta_and_stoppedViolation_measure_le_of_aeAlignedWindowPositiveActionCostBudgetExhaustionTime {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) (window budget : Nat) (hwindow : AlignedWindowPositiveActionCostAE (Thompson.canonicalHistoryTrajectoryMeasure (OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) actionCost window) : 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