Lean module · OFUL
BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretSecondMoment
# Explicit second-moment unbounded stopping-time OFUL expected-regret rate This module integrates the quadratic stopped-budget envelope. The canonical terminal theorem therefore depends only on the supplied round-count second moment, not on an unevaluated expected stopped-budget term.
Module map
Imports
BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretClosed
Imported by
BanditRLProof, BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretExactMoment
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.integral_stoppedValue_telescopingHighProbabilityPseudoRegretBound_le_quadraticCoefficient_mul_roundSecondMoment_of_squareIntegrableFiniteStoppingTime
Compiled
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
theorem
BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_roundSecondMoment_add_initialGap_mul_sqrt_roundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime
Compiled
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