BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretClosed

The scalar log-determinant budget is at most linear in the round count.

theorem standardScalarLogDetBudget_le_rounds_mul_div {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (rounds : Nat) (L2 : Real) (hL2 : 0 <= L2) : standardScalarLogDetBudget (Feature

Parameter-only coefficient in the quadratic envelope for the explicit telescoping pseudo-regret budget.

noncomputable def telescopingHighProbabilityPseudoRegretQuadraticCoefficient {Feature : Type u} [Fintype Feature] (R delta lambda S L2 : Real) : Real

The quadratic-envelope coefficient is nonnegative.

theorem telescopingHighProbabilityPseudoRegretQuadraticCoefficient_nonneg {Feature : Type u} [Fintype Feature] (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (hS : 0 <= S) (L2 : Real) (hL2 : 0 <= L2) : 0 <= telescopingHighProbabilityPseudoRegretQuadraticCoefficient (Feature

The telescoping confidence logarithm is bounded by a parameter-only coefficient times the square of the round count.

theorem telescopingHighProbabilityRegretLogBudget_le_rounds_sq_mul {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (delta : Real) (hdelta : 0 < delta) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : telescopingHighProbabilityRegretLogBudget (Feature

The explicit telescoping pseudo-regret budget grows at most quadratically in the round count.

theorem telescopingHighProbabilityPseudoRegretBound_le_rounds_sq_mul_coefficient {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : telescopingHighProbabilityPseudoRegretBound (Feature

Square-integrability of the stopping-time round count automatically makes the stopped explicit telescoping pseudo-regret budget integrable.

theorem integrable_stoppedValue_telescopingHighProbabilityPseudoRegretBound_of_squareIntegrableFiniteStoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] [Nonempty Feature] (mu : Measure (Nat -> Fin K × Real)) (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (hS : 0 <= S) (L2 : Real) (hL2 : 0 <= L2) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

Canonical square-integrable unbounded-stopping expected pseudo-regret rate with stopped-budget integrability discharged automatically.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_integral_stoppedBudget_add_initialGap_mul_sqrt_roundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime_automaticBudgetIntegrability {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 : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K