BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · OFUL

BanditRLProof.OFULExpectedRegretAsymptotics

This module upgrades the explicit finite-window canonical OFUL expected pseudo-regret theorem to an IsBigO statement at Filter.atTop. The feature dimension and model parameters are fixed while the horizon varies.

Module map

Declarations
7
Placeholders
0

Imports

BanditRLProof.OFULExpectedRegretRate

Imported by

BanditRLProof, BanditRLProof.OFULExpectedRegretConsistency, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretAsymptotics

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

theorem BanditRLProof.OFUL.standardScalarLogDetBudget_isBigO_log 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 identitydeclaration:BanditRLProof.OFUL.standardScalarLogDetBudget_isBigO_log

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem standardScalarLogDetBudget_isBigO_log {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (L2 : Real) (hL2 : 0 <= L2) : (fun horizon : Nat => standardScalarLogDetBudget (Feature := Feature) lambda (horizon + 1) L2) =O[atTop] (fun horizon : Nat => Real.log (((horizon + 1 : Nat) : Real)))
Source line 21 Chapter context: OFUL
theorem BanditRLProof.OFUL.standardExpectedRegretLogBudget_isBigO_log 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 identitydeclaration:BanditRLProof.OFUL.standardExpectedRegretLogBudget_isBigO_log

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem standardExpectedRegretLogBudget_isBigO_log {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (L2 : Real) (hL2 : 0 <= L2) : (fun horizon : Nat => standardExpectedRegretLogBudget (Feature := Feature) lambda horizon L2) =O[atTop] (fun horizon : Nat => Real.log (((horizon + 1 : Nat) : Real)))
Source line 80 Chapter context: OFUL
theorem BanditRLProof.OFUL.sqrt_log_succ_isBigO_log_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 identitydeclaration:BanditRLProof.OFUL.sqrt_log_succ_isBigO_log_succ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem sqrt_log_succ_isBigO_log_succ : (fun horizon : Nat => Real.sqrt (Real.log (((horizon + 1 : Nat) : Real)))) =O[atTop] (fun horizon : Nat => Real.log (((horizon + 1 : Nat) : Real)))
Source line 101 Chapter context: OFUL
theorem BanditRLProof.OFUL.standardExpectedPseudoRegretBound_isBigO_sqrt_mul_log 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 identitydeclaration:BanditRLProof.OFUL.standardExpectedPseudoRegretBound_isBigO_sqrt_mul_log

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem standardExpectedPseudoRegretBound_isBigO_sqrt_mul_log {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 => Real.sqrt (((horizon + 1 : Nat) : Real)) * Real.log (((horizon + 1 : Nat) : Real)))
Source line 126 Chapter context: OFUL
def BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret 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 identitydeclaration:BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def canonicalStandardExpectedPseudoRegret {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
Source line 247 Chapter context: OFUL
theorem BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_nonneg_and_le 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 identitydeclaration:BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_nonneg_and_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem canonicalStandardExpectedPseudoRegret_nonneg_and_le {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) (horizon : Nat) (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) : 0 <= canonicalStandardExpectedPseudoRegret hK lambda thetaStar actionFeature R S environment best horizon ∧ canonicalStandardExpectedPseudoRegret hK lambda thetaStar actionFeature R S environment best horizon <= standardExpectedPseudoRegretBound (Feature := Feature) R lambda S horizon L2
Source line 267 Chapter context: OFUL
theorem BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_isBigO_sqrt_mul_log 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 identitydeclaration:BanditRLProof.OFUL.canonicalStandardExpectedPseudoRegret_isBigO_sqrt_mul_log

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem canonicalStandardExpectedPseudoRegret_isBigO_sqrt_mul_log {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 => Real.sqrt (((horizon + 1 : Nat) : Real)) * Real.log (((horizon + 1 : Nat) : Real)))
Source line 296 Chapter context: OFUL