Lean module · OFUL
BanditRLProof.OFULExpectedRegretConsistency
This module turns the fixed-model asymptotic expected pseudo-regret bound into convergence of expected pseudo-regret per played round. The generated algorithm still uses the horizon-dependent parameter 1 / (T + 1)^2.
Module map
Imports
BanditRLProof.OFULExpectedRegretAsymptotics
Imported by
BanditRLProof, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretConsistency, BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityAverageRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.sqrt_mul_log_succ_isLittleO_natCast_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sqrt_mul_log_succ_isLittleO_natCast_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sqrt_mul_log_succ_isLittleO_natCast_succ : (fun horizon : Nat => Real.sqrt (((horizon + 1 : Nat) : Real)) * Real.log (((horizon + 1 : Nat) : Real))) =o[atTop] (fun horizon : Nat => (((horizon + 1 : Nat) : Real)))
theorem
BanditRLProof.OFUL.standardExpectedPseudoRegretBound_isLittleO_natCast_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.standardExpectedPseudoRegretBound_isLittleO_natCast_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem standardExpectedPseudoRegretBound_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 => standardExpectedPseudoRegretBound (Feature := Feature) R lambda S horizon L2) =o[atTop] (fun horizon : Nat => (((horizon + 1 : Nat) : Real)))
theorem
BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_isLittleO_natCast_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_isLittleO_natCast_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonicalStandardExpectedPseudoRegret_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) : (canonicalStandardExpectedPseudoRegret hK lambda thetaStar actionFeature R S environment best) =o[atTop] (fun horizon : Nat => (((horizon + 1 : Nat) : Real)))
def
BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def canonicalStandardExpectedAveragePseudoRegret {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) (horizon : Nat) : Real
theorem
BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret_tendsto_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret_tendsto_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonicalStandardExpectedAveragePseudoRegret_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) : Tendsto (canonicalStandardExpectedAveragePseudoRegret hK lambda thetaStar actionFeature R S environment best) atTop (nhds 0)