Lean module · OFUL
BanditRLProof.OFULEllipticalPotentialFoundation
This module packages the determinant-growth and clipped inverse-quadratic conclusions of the deterministic OFUL linear-algebra route in one theorem-facing statement. It is the handoff expected by a later self-normalized concentration and confidence-ellipsoid proof.
Module map
Imports
BanditRLProof.OFULEllipticalPotential
Imported by
BanditRLProof, BanditRLProof.OFULSelectedWidthSummation, BanditRLProof.OFULSelfNormalizedConfidence
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.standardLogDeterminantAndEllipticalPotential
Compiled
Standard logarithmic determinant and elliptical-potential bounds. For a positive scalar regularization and uniformly bounded squared feature norms, the terminal regularized Gram determinant and the cumulative clipped inverse-quadratic updates are controlled by `d * log (1 + T * L2 / (d * lambda))`.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.standardLogDeterminantAndEllipticalPotentialReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem standardLogDeterminantAndEllipticalPotential {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 : Nat, t < T -> dotProduct (history t) (history t) <= L2) : (regularizedPrefixFeatureGram lambda history T).det <= lambda ^ Fintype.card Feature * Real.exp ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda))) /\ (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda)))