BanditRLProof.OFULFiniteActionOptimism

The inverse-Gram confidence width of one feature vector.

noncomputable def confidenceWidth [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (x : Feature -> Real) : Real

Linear value of a feature vector under a parameter.

def linearValue [Fintype Feature] (theta x : Feature -> Real) : Real

OFUL upper-confidence score `thetaHat dot x + beta * ||x||_(V⁻¹)`.

noncomputable def optimisticScore [Fintype Feature] [DecidableEq Feature] (thetaHat : Feature -> Real) (V : Matrix Feature Feature Real) (beta : Real) (x : Feature -> Real) : Real

A finite nonempty type admits a score-maximizing action.

noncomputable def finiteActionArgmax [Finite Action] [Nonempty Action] (score : Action -> Real) : Action

The finite-action argmax dominates every action score.

theorem finiteActionArgmax_spec [Finite Action] [Nonempty Action] (score : Action -> Real) (action : Action) : score action <= score (finiteActionArgmax score)

Weighted Cauchy-Schwarz: the ordinary dot product is controlled by the `V`-norm and inverse-`V` confidence width.

theorem abs_dotProduct_le_matrixNorm_mul_confidenceWidth [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (error x : Feature -> Real) : |dotProduct error x| <= matrixNorm V error * confidenceWidth V x

On a confidence ellipsoid, every true linear action value lies below its upper-confidence score.

theorem linearValue_le_optimisticScore_of_matrixNorm_sub_le [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (thetaHat thetaStar : Feature -> Real) (beta : Real) (x : Feature -> Real) (hconfidence : matrixNorm V (thetaHat - thetaStar) <= beta) : linearValue thetaStar x <= optimisticScore thetaHat V beta x

On the same confidence ellipsoid, every upper-confidence score is at most the true value plus twice its confidence bonus.

theorem optimisticScore_le_linearValue_add_two_mul_bonus_of_matrixNorm_sub_le [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (thetaHat thetaStar : Feature -> Real) (beta : Real) (x : Feature -> Real) (hconfidence : matrixNorm V (thetaHat - thetaStar) <= beta) : optimisticScore thetaHat V beta x <= linearValue thetaStar x + 2 * beta * confidenceWidth V x

The score-maximizing finite action for the OFUL upper-confidence score.

noncomputable def finiteActionOptimisticChoice [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (thetaHat : Feature -> Real) (V : Matrix Feature Feature Real) (beta : Real) (actionFeature : Action -> Feature -> Real) : Action

The finite OFUL choice maximizes the optimistic score.

theorem finiteActionOptimisticChoice_score_max [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (thetaHat : Feature -> Real) (V : Matrix Feature Feature Real) (beta : Real) (actionFeature : Action -> Feature -> Real) (action : Action) : optimisticScore thetaHat V beta (actionFeature action) <= optimisticScore thetaHat V beta (actionFeature (finiteActionOptimisticChoice thetaHat V beta actionFeature))

On the confidence ellipsoid, the true value gap between any comparator and the finite optimistic choice is at most twice the chosen action's bonus.

theorem linearValue_sub_finiteActionOptimisticChoice_le_two_mul_bonus [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (V : Matrix Feature Feature Real) (hV : V.PosDef) (thetaHat thetaStar : Feature -> Real) (beta : Real) (actionFeature : Action -> Feature -> Real) (hconfidence : matrixNorm V (thetaHat - thetaStar) <= beta) (action : Action) : linearValue thetaStar (actionFeature action) - linearValue thetaStar (actionFeature (finiteActionOptimisticChoice thetaHat V beta actionFeature)) <= 2 * beta * confidenceWidth V (actionFeature (finiteActionOptimisticChoice thetaHat V beta actionFeature))

Scalar-regularized finite-horizon Gram matrix used by OFUL selection.

noncomputable def finiteHorizonScalarGram [Fintype Feature] [DecidableEq Feature] (lambda : Real) (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : Matrix Feature Feature Real

Finite-action OFUL choice using the scalar-ridge estimate and the compiled scalar confidence radius.

noncomputable def finiteHorizonScalarOptimisticAction [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (candidateFeature : Omega -> Action -> Feature -> Real) (R delta S : Real) (n : Nat) (omega : Omega) : Action

Pointwise finite-horizon optimism: on the scalar confidence ellipsoid, every comparator's true linear value exceeds the selected value by at most twice the selected confidence bonus.

theorem finiteHorizonScalarOptimisticAction_gap_le [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (candidateFeature : Omega -> Action -> Feature -> Real) (R delta : Real) (n : Nat) (omega : Omega) (hconfidence : matrixNorm (finiteHorizonScalarGram lambda feature n omega) (finiteHorizonRidgeEstimate (Matrix.scalar Feature lambda) feature response n omega - thetaStar) <= finiteHorizonScalarConfidenceRadius feature R delta lambda S n omega) (action : Action) : linearValue thetaStar (candidateFeature omega action) - linearValue thetaStar (candidateFeature omega (finiteHorizonScalarOptimisticAction lambda feature response candidateFeature R delta S n omega)) <= 2 * finiteHorizonScalarConfidenceRadius feature R delta lambda S n omega * confidenceWidth (finiteHorizonScalarGram lambda feature n omega) (candidateFeature omega (finiteHorizonScalarOptimisticAction lambda feature response candidateFeature R delta S n omega))

The event that some finite candidate action violates the one-step OFUL gap certificate.

noncomputable def finiteHorizonScalarOptimismViolationSet [Finite Action] [Nonempty Action] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (candidateFeature : Omega -> Action -> Feature -> Real) (R delta : Real) (n : Nat) : Set Omega

Finite-action OFUL optimism violation has probability at most `delta`. No measurability of the candidate features or selected action is required: the violation event is included pointwise in the already controlled scalar confidence-ellipsoid bad event.

theorem measure_finiteHorizonScalarOptimismViolationSet_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Finite Action] [Nonempty Action] [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) (candidateFeature : Omega -> Action -> Feature -> 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 (finiteHorizonScalarOptimismViolationSet lambda thetaStar S feature response candidateFeature R delta n) <= ENNReal.ofReal delta