BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretSecondMoment

The expected stopped explicit telescoping budget is controlled by the same round-count second moment used by the bad-event overflow bound.

theorem integral_stoppedValue_telescopingHighProbabilityPseudoRegretBound_le_quadraticCoefficient_mul_roundSecondMoment_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 := K)) tau) (hstop : SquareIntegrableFiniteStoppingTime mu tau) (roundSecondMoment : Real) (hroundSecondMoment : integral mu (fun trajectory => ((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) <= roundSecondMoment) : integral mu (stoppedValue (fun horizon (_trajectory : Nat -> Fin K × Real) => telescopingHighProbabilityPseudoRegretBound (Feature := Feature) R delta lambda S horizon L2) tau) <= telescopingHighProbabilityPseudoRegretQuadraticCoefficient (Feature := Feature) R delta lambda S L2 * roundSecondMoment

Canonical generated-trajectory unbounded-stopping expected pseudo-regret bound with every stopped-budget term replaced by an explicit second-moment charge.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_roundSecondMoment_add_initialGap_mul_sqrt_roundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime {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 := K)) tau) (hstop : SquareIntegrableFiniteStoppingTime (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) tau) (roundSecondMoment : Real) (hroundSecondMoment : integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) (fun trajectory => ((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) <= roundSecondMoment) : let mu := Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment let stoppedRegret := stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau let bad := telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau 0 <= integral mu stoppedRegret ∧ integral mu stoppedRegret <= telescopingHighProbabilityPseudoRegretQuadraticCoefficient (Feature := Feature) R delta lambda S L2 * roundSecondMoment + standardScalarInitialGapBound S L2 * Real.sqrt roundSecondMoment * Real.sqrt delta ∧ mu bad <= ENNReal.ofReal delta