Lean module · OFUL
BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretExactMoment
# Exact-second-moment unbounded stopping-time OFUL expected-regret rate 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.
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.
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.
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