BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · OFUL

BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegret

# Bounded stopping-time expected OFUL pseudo-regret rate This module integrates the compiled bounded-stopping-time high-probability pseudo-regret theorem. Horizon monotonicity moves both the explicit scheduled budget and the deterministic gap envelope to the deterministic stopping-time bound. The expectation proof is an indicator decomposition, not optional stopping.

Module map

Declarations
9
Placeholders
0

Imports

BanditRLProof.OFULExpectedRegret, BanditRLProof.OFULScheduledBoundedStoppingTimeHighProbabilityRegretRate

Imported by

BanditRLProof, BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretRate, BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegret

Declarations

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

theorem BanditRLProof.OFUL.telescopingHighProbabilityRegretLogBudget_nonneg Compiled

The explicit telescoping confidence logarithm is nonnegative.

theorem telescopingHighProbabilityRegretLogBudget_nonneg {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : 0 <= telescopingHighProbabilityRegretLogBudget (Feature
Source line 23 Chapter context: OFUL
theorem BanditRLProof.OFUL.telescopingHighProbabilityRegretLogBudget_mono Compiled

The explicit telescoping confidence logarithm is monotone in the horizon.

theorem telescopingHighProbabilityRegretLogBudget_mono {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (delta : Real) (hdelta : 0 < delta) (L2 : Real) (hL2 : 0 <= L2) {n horizon : Nat} (hn : n <= horizon) : telescopingHighProbabilityRegretLogBudget (Feature
Source line 59 Chapter context: OFUL
theorem BanditRLProof.OFUL.telescopingHighProbabilityPseudoRegretBound_nonneg Compiled

The explicit telescoping pseudo-regret budget is nonnegative.

theorem telescopingHighProbabilityPseudoRegretBound_nonneg {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) : 0 <= telescopingHighProbabilityPseudoRegretBound (Feature
Source line 110 Chapter context: OFUL
theorem BanditRLProof.OFUL.telescopingHighProbabilityPseudoRegretBound_mono Compiled

The explicit telescoping pseudo-regret budget is monotone in the horizon.

theorem telescopingHighProbabilityPseudoRegretBound_mono {Feature : Type u} [Fintype Feature] [Nonempty Feature] (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (lambda : Real) (hlambda : 0 < lambda) (S : Real) (hS : 0 <= S) (L2 : Real) (hL2 : 0 <= L2) {n horizon : Nat} (hn : n <= horizon) : telescopingHighProbabilityPseudoRegretBound (Feature
Source line 127 Chapter context: OFUL
theorem BanditRLProof.OFUL.standardScalarAllRoundGapEnvelope_mono Compiled

The deterministic all-round gap envelope is monotone in the horizon.

theorem standardScalarAllRoundGapEnvelope_mono (S : Real) (hS : 0 <= S) (L2 : Real) {n horizon : Nat} (hn : n <= horizon) : standardScalarAllRoundGapEnvelope S n L2 <= standardScalarAllRoundGapEnvelope S horizon L2
Source line 206 Chapter context: OFUL
theorem BanditRLProof.OFUL.abs_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_envelope Compiled

A bounded stopped pseudo-regret obeys the endpoint gap envelope.

theorem abs_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_envelope {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (maxHorizon : Nat) (htau_le : forall trajectory, tau trajectory <= (maxHorizon : WithTop Nat)) (trajectory : Nat -> Fin K × Real) : |stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau trajectory| <= standardScalarAllRoundGapEnvelope S maxHorizon L2
Source line 222 Chapter context: OFUL
theorem BanditRLProof.OFUL.integrable_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_of_boundedStoppingTime Compiled

A bounded stopped pseudo-regret is integrable under a finite measure.

theorem integrable_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_of_boundedStoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] (mu : Measure (Nat -> Fin K × Real)) [IsFiniteMeasure mu] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K
Source line 268 Chapter context: OFUL
theorem BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_endpoint_add_envelope_mul_real_measure Compiled

Generic stopped expectation assembly: off the stopped violation event, the stopped regret is below the endpoint explicit budget; on the event it is charged by the endpoint deterministic envelope.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_endpoint_add_envelope_mul_real_measure {K : Nat} {Feature : Type u} [Fintype Feature] [Nonempty Feature] (mu : Measure (Nat -> Fin K × Real)) [IsProbabilityMeasure mu] (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) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K
Source line 325 Chapter context: OFUL
theorem BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_endpoint_add_envelope_mul_delta_of_linearSubgaussianEnvironment_of_featureBound_le_regularization Compiled

Complete bounded-stopping-time expected pseudo-regret theorem for the single telescoping-schedule OFUL policy.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_endpoint_add_envelope_mul_delta_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) (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
Source line 491 Chapter context: OFUL