Lean module · OFUL

BanditRLProof.OFULSelectedWidthSummation

# Selected-width summation for OFUL This module converts the compiled logarithmic elliptical-potential endpoint into cumulative clipped confidence-width bounds for arbitrary feature and selected-action sequences. The route is deterministic and finite-horizon.

Module map

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

Imports

BanditRLProof.OFULFiniteActionOptimism, BanditRLProof.OFULEllipticalPotentialFoundation

Imported by

BanditRLProof, BanditRLProof.OFULGeneratedTrajectoryRadiusWidth

Declarations

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

def BanditRLProof.OFUL.clippedConfidenceWidth Compiled

The confidence width clipped at the inverse-quadratic level. This equals `min 1 (confidenceWidth V x)` when `V` is positive definite.

noncomputable def clippedConfidenceWidth {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (x : Feature -> Real) : Real

Source line 21 Chapter context: OFUL

theorem BanditRLProof.OFUL.clippedConfidenceWidth_eq_min_one_confidenceWidth Compiled

Clipping before the square root agrees with clipping the confidence width.

theorem clippedConfidenceWidth_eq_min_one_confidenceWidth {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (x : Feature -> Real) : clippedConfidenceWidth V x = min 1 (confidenceWidth V x)

Source line 27 Chapter context: OFUL

theorem BanditRLProof.OFUL.sum_range_clippedConfidenceWidth_le_sqrt_mul_sqrt_log Compiled

The cumulative clipped widths of a bounded feature sequence are controlled by the square root of the standard logarithmic elliptical-potential budget.

theorem sum_range_clippedConfidenceWidth_le_sqrt_mul_sqrt_log {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (history t) (history t) <= L2) : (Finset.range T).sum (fun t => clippedConfidenceWidth (regularizedPrefixFeatureGram lambda history t) (history t)) <= Real.sqrt (T : Real) * Real.sqrt (2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))))

Source line 46 Chapter context: OFUL

theorem BanditRLProof.OFUL.sum_range_min_one_confidenceWidth_le_sqrt_mul_sqrt_log Compiled

Public confidence-width form of the clipped selected-feature sum bound.

theorem sum_range_min_one_confidenceWidth_le_sqrt_mul_sqrt_log {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (history t) (history t) <= L2) : (Finset.range T).sum (fun t => min 1 (confidenceWidth (regularizedPrefixFeatureGram lambda history t) (history t))) <= Real.sqrt (T : Real) * Real.sqrt (2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))))

Source line 112 Chapter context: OFUL

theorem BanditRLProof.OFUL.sum_range_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_one Compiled

Raw selected-feature widths satisfy the same bound when every charged width is at most one.

theorem sum_range_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (history t) (history t) <= L2) (hwidth : forall t, t < T -> confidenceWidth (regularizedPrefixFeatureGram lambda history t) (history t) <= 1) : (Finset.range T).sum (fun t => confidenceWidth (regularizedPrefixFeatureGram lambda history t) (history t)) <= Real.sqrt (T : Real) * Real.sqrt (2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))))

Source line 155 Chapter context: OFUL

theorem BanditRLProof.OFUL.sum_range_selectedAction_min_one_confidenceWidth_le_sqrt_mul_sqrt_log Compiled

Selected-action specialization of the cumulative clipped confidence-width bound.

theorem sum_range_selectedAction_min_one_confidenceWidth_le_sqrt_mul_sqrt_log {Feature : Type u} {Action : Type v} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Action -> Feature -> Real) (selectedAction : Nat -> Action) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (actionFeature (selectedAction t)) (actionFeature (selectedAction t)) <= L2) : (Finset.range T).sum (fun t => min 1 (confidenceWidth (regularizedPrefixFeatureGram lambda (fun s => actionFeature (selectedAction s)) t) (actionFeature (selectedAction t)))) <= Real.sqrt (T : Real) * Real.sqrt (2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))))

Source line 194 Chapter context: OFUL

theorem BanditRLProof.OFUL.sum_range_selectedAction_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_one Compiled

Raw selected-action width sum under an explicit small-width contract.

theorem sum_range_selectedAction_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_one {Feature : Type u} {Action : Type v} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Action -> Feature -> Real) (selectedAction : Nat -> Action) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t, t < T -> dotProduct (actionFeature (selectedAction t)) (actionFeature (selectedAction t)) <= L2) (hwidth : forall t, t < T -> confidenceWidth (regularizedPrefixFeatureGram lambda (fun s => actionFeature (selectedAction s)) t) (actionFeature (selectedAction t)) <= 1) : (Finset.range T).sum (fun t => confidenceWidth (regularizedPrefixFeatureGram lambda (fun s => actionFeature (selectedAction s)) t) (actionFeature (selectedAction t))) <= Real.sqrt (T : Real) * Real.sqrt (2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))))

Source line 222 Chapter context: OFUL