Lean module · OFUL
BanditRLProof.OFULSelectedWidthSummation
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
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.clippedConfidenceWidthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def clippedConfidenceWidth {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (x : Feature -> Real) : Real
theorem
BanditRLProof.OFUL.clippedConfidenceWidth_eq_min_one_confidenceWidth
Compiled
Clipping before the square root agrees with clipping the confidence width.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.clippedConfidenceWidth_eq_min_one_confidenceWidthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sum_range_clippedConfidenceWidth_le_sqrt_mul_sqrt_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))))
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sum_range_min_one_confidenceWidth_le_sqrt_mul_sqrt_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))))
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sum_range_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))))
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sum_range_selectedAction_min_one_confidenceWidth_le_sqrt_mul_sqrt_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))))
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.sum_range_selectedAction_confidenceWidth_le_sqrt_mul_sqrt_log_of_width_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))))