Lean module · OFUL
BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretConsistency
# Expected-average consistency for bounded-stopping-time OFUL This module normalizes the fixed-model horizon-indexed expected stopped pseudo-regret family by the number of available rounds. The policy at horizon `T` retains the telescoping schedule with outer budget `1 / (T + 1)`.
Module map
Imports
BanditRLProof.OFULExpectedRegretConsistency, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretAsymptotics
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.telescopingStandardExpectedPseudoRegretBound_isLittleO_natCast_succ
Compiled
The explicit tuned bounded-stopping-time expected pseudo-regret budget is `o(T + 1)`.
theorem telescopingStandardExpectedPseudoRegretBound_isLittleO_natCast_succ {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (L2 : Real) (hL2 : 0 <= L2) : (fun horizon : Nat => telescopingStandardExpectedPseudoRegretBound (Feature
theorem
BanditRLProof.OFUL.canonicalTelescopingStandardExpectedStoppedPseudoRegret_isLittleO_natCast_succ
Compiled
For fixed model parameters and a horizon-indexed stopping-time family bounded by its horizon, the named expected stopped pseudo-regret is `o(T + 1)`.
theorem canonicalTelescopingStandardExpectedStoppedPseudoRegret_isLittleO_natCast_succ {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) (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 -> (Nat -> Fin K × Real) -> WithTop Nat) (htau : forall maxHorizon, IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K
def
BanditRLProof.OFUL.canonicalTelescopingStandardExpectedAverageStoppedPseudoRegret
Compiled
The expected stopped pseudo-regret per available round for the horizon-indexed telescoping-schedule policy and stopping-time family.
noncomputable def canonicalTelescopingStandardExpectedAverageStoppedPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (best : Fin K) (tau : Nat -> (Nat -> Fin K × Real) -> WithTop Nat) (horizon : Nat) : Real
theorem
BanditRLProof.OFUL.canonicalTelescopingStandardExpectedAverageStoppedPseudoRegret_tendsto_zero
Compiled
For fixed model parameters and any horizon-indexed canonical stopping-time family bounded pointwise by its horizon, expected stopped pseudo-regret per available round converges to zero.
theorem canonicalTelescopingStandardExpectedAverageStoppedPseudoRegret_tendsto_zero {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) (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 -> (Nat -> Fin K × Real) -> WithTop Nat) (htau : forall maxHorizon, IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K