BanditRLProof.OFULScalarRegularizationBias

The Euclidean length written on the same finite-coordinate surface as `dotProduct`.

noncomputable def euclideanLength [Fintype Feature] (theta : Feature -> Real) : Real

A positive scalar multiple of the identity is positive definite.

theorem scalarIdentity_posDef [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) : (Matrix.scalar Feature lambda : Matrix Feature Feature Real).PosDef

For `V = lambda I + G` with `G` positive semidefinite, the `V`-norm of the ridge bias `V⁻¹ (lambda theta)` is at most `sqrt lambda * ‖theta‖₂`.

theorem matrixNorm_nonsingInv_scalar_mulVec_le_sqrt_mul_euclideanLength [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (G : Matrix Feature Feature Real) (hG : G.PosSemidef) (theta : Feature -> Real) : matrixNorm (Matrix.scalar Feature lambda + G) ((Matrix.scalar Feature lambda + G)⁻¹.mulVec ((Matrix.scalar Feature lambda).mulVec theta)) <= Real.sqrt lambda * euclideanLength theta

The standard scalar-regularized OFUL radius `noise radius + sqrt lambda * S`.

noncomputable def finiteHorizonScalarConfidenceRadius [Fintype Feature] [DecidableEq Feature] (feature : Nat -> Omega -> Feature -> Real) (R delta lambda S : Real) (n : Nat) (omega : Omega) : Real

The scalar regularization bias is uniformly bounded by `sqrt lambda * S` whenever the true parameter has Euclidean length at most `S`.

theorem finiteHorizon_scalarRegularizationBias_le [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (S : Real) (htheta : euclideanLength thetaStar <= S) (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : matrixNorm (Matrix.scalar Feature lambda + finiteHorizonFeatureGram feature n omega) ((Matrix.scalar Feature lambda + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec ((Matrix.scalar Feature lambda).mulVec thetaStar)) <= Real.sqrt lambda * S

Finite-horizon OFUL confidence ellipsoid with scalar ridge regularization. The explicit bias premise of the general theorem is discharged from `euclideanLength thetaStar <= S`.

theorem measure_finiteHorizonScalarRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (S : Real) (htheta : euclideanLength thetaStar <= S) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (R : Real) (hR : 0 < R) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (hresponse : forall omega i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) : mu {omega | matrixNorm (Matrix.scalar Feature lambda + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate (Matrix.scalar Feature lambda) feature response n omega - thetaStar) > finiteHorizonScalarConfidenceRadius feature R delta lambda S n omega} <= ENNReal.ofReal delta