Lean module · OFUL

BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretRate

# Explicit bounded-stopping-time expected OFUL pseudo-regret rate This module tunes the outer confidence budget of the scheduled bounded stopping-time expectation theorem to `1 / (T + 1)`. The stopped bad-event charge becomes one initial-gap envelope, while the scheduled confidence logarithm remains explicit.

Module map

Source: BanditRLProof/OFULScheduledBoundedStoppingTimeExpectedRegretRate.lean
Teaching chapter: 5. OFUL, self-normalized confidence, and stopping times
Declarations: 7
Placeholders: 0

Imports

BanditRLProof.OFULExpectedRegretRate, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegret

Imported by

BanditRLProof, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretAsymptotics

Declarations

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

def BanditRLProof.OFUL.telescopingStandardExpectedRegretLogBudget Compiled

The explicit scheduled confidence logarithm after choosing the outer expected-regret budget `delta_T = 1 / (T + 1)`.

noncomputable def telescopingStandardExpectedRegretLogBudget {Feature : Type u} [Fintype Feature] (lambda : Real) (horizon : Nat) (L2 : Real) : Real

Source line 24 Chapter context: OFUL

theorem BanditRLProof.OFUL.telescopingHighProbabilityRegretLogBudget_standardExpectedRegretDelta Compiled

Substituting `delta_T = 1 / (T + 1)` into the scheduled confidence logarithm gives the explicit cubic-in-horizon logarithmic scale.

theorem telescopingHighProbabilityRegretLogBudget_standardExpectedRegretDelta {Feature : Type u} [Fintype Feature] (lambda : Real) (horizon : Nat) (L2 : Real) : telescopingHighProbabilityRegretLogBudget (Feature

Source line 37 Chapter context: OFUL

def BanditRLProof.OFUL.telescopingStandardExpectedPseudoRegretBound Compiled

Explicit expected pseudo-regret budget for a stopping time bounded by `T` under the single scheduled policy tuned with outer budget `1 / (T + 1)`.

noncomputable def telescopingStandardExpectedPseudoRegretBound {Feature : Type u} [Fintype Feature] (R lambda S : Real) (horizon : Nat) (L2 : Real) : Real

Source line 62 Chapter context: OFUL

theorem BanditRLProof.OFUL.telescopingHighProbabilityPseudoRegretBound_add_initial_standardExpectedRegretDelta_eq Compiled

The endpoint high-probability budget plus the tuned bad-event envelope charge is exactly the explicit scheduled expected pseudo-regret rate.

theorem telescopingHighProbabilityPseudoRegretBound_add_initial_standardExpectedRegretDelta_eq {Feature : Type u} [Fintype Feature] (R lambda S : Real) (horizon : Nat) (L2 : Real) : telescopingHighProbabilityPseudoRegretBound (Feature

Source line 81 Chapter context: OFUL

theorem

BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_telescopingStandardExpectedBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization

Compiled

Complete explicit expected pseudo-regret theorem for one bounded stopping time under the horizon-tuned telescoping-schedule OFUL policy.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_telescopingStandardExpectedBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization {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 -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

Source line 104 Chapter context: OFUL

def BanditRLProof.OFUL.canonicalTelescopingStandardExpectedStoppedPseudoRegret Compiled

Expected stopped pseudo-regret for the horizon-indexed family of scheduled policies tuned at `delta_T = 1 / (T + 1)`.

noncomputable def canonicalTelescopingStandardExpectedStoppedPseudoRegret {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) (maxHorizon : Nat) : Real

Source line 164 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalTelescopingStandardExpectedStoppedPseudoRegret_nonneg_and_le Compiled

The named horizon-indexed expected stopped pseudo-regret is nonnegative and bounded pointwise by the explicit tuned scheduled rate.

theorem canonicalTelescopingStandardExpectedStoppedPseudoRegret_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) (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

Source line 192 Chapter context: OFUL