Lean module · OFUL
BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretExactMoment
This module names the actual second moment of the stopping-time round count and uses it directly in the canonical terminal theorem. Concrete stopping-rule analyses can subsequently bound this named quantity without rebuilding the stopped-regret argument.
Module map
Imports
BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretSecondMoment
Imported by
BanditRLProof, BanditRLProof.OFULScheduledBudgetExhaustionExpectedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.OFUL.stoppingTimeRoundSecondMoment
Compiled
The actual second moment of the real round count `tau.untopA + 1` under the square-integrable finite-stopping contract.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.stoppingTimeRoundSecondMomentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def stoppingTimeRoundSecondMoment {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) (tau : Omega -> WithTop Nat) (_hstop : SquareIntegrableFiniteStoppingTime mu tau) : Real
theorem
BanditRLProof.OFUL.stoppingTimeRoundSecondMoment_nonneg
Compiled
The exact stopping-time round-count second moment is nonnegative.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.stoppingTimeRoundSecondMoment_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem stoppingTimeRoundSecondMoment_nonneg {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) (tau : Omega -> WithTop Nat) (hstop : SquareIntegrableFiniteStoppingTime mu tau) : 0 <= stoppingTimeRoundSecondMoment mu tau hstop
theorem
BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime
Compiled
Canonical generated-trajectory unbounded-stopping expected pseudo-regret bound stated directly with the actual round-count second moment.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTimeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_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) : 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 * stoppingTimeRoundSecondMoment mu tau hstop + standardScalarInitialGapBound S L2 * Real.sqrt (stoppingTimeRoundSecondMoment mu tau hstop) * Real.sqrt delta ∧ mu bad <= ENNReal.ofReal delta