Lean module · OFUL
BanditRLProof.OFULEllipticalPotentialFoundation
# Standard OFUL elliptical-potential endpoint 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))`.
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)))