Lean module · OFUL

BanditRLProof.OFULConfidenceEllipsoid

This module consumes the common-R vector self-normalized tail. It defines the finite-horizon ridge estimator from scalar observations, proves its exact error decomposition into the martingale score and regularization bias, and transports the score tail to a parameter confidence ellipsoid.

Module map

Source: BanditRLProof/OFULConfidenceEllipsoid.lean
Teaching chapter: 5. OFUL, self-normalized confidence, and stopping times
Declarations: 18
Placeholders: 0

Imports

BanditRLProof.OFULSelfNormalizedMarkov

Imported by

BanditRLProof, BanditRLProof.OFULScalarRegularizationBias

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.OFUL.matrixNorm Compiled

Quadratic-form square root; it is a norm when the matrix is positive definite.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.matrixNorm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def matrixNorm [Fintype Feature] (A : Matrix Feature Feature Real) (x : Feature -> Real) : Real

Source line 20 Chapter context: OFUL

theorem BanditRLProof.OFUL.matrixNorm_add_le Compiled

Triangle inequality for the norm induced by a positive-definite matrix.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.matrixNorm_add_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem matrixNorm_add_le [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x y : Feature -> Real) : matrixNorm A (x + y) <= matrixNorm A x + matrixNorm A y

Source line 26 Chapter context: OFUL

theorem BanditRLProof.OFUL.matrixNorm_sub_le Compiled

Triangle inequality for subtraction in a positive-definite matrix norm.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.matrixNorm_sub_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem matrixNorm_sub_le [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x y : Feature -> Real) : matrixNorm A (x - y) <= matrixNorm A x + matrixNorm A y

Source line 43 Chapter context: OFUL

theorem BanditRLProof.OFUL.matrixNorm_sq Compiled

Squaring the positive-definite matrix norm recovers its quadratic form.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.matrixNorm_sq

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem matrixNorm_sq [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x : Feature -> Real) : matrixNorm A x ^ 2 = x ⬝ᵥ A.mulVec x

Source line 60 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonResponseVector Compiled

The finite-horizon sufficient statistic `sum_{i<n} x_i y_i`.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonResponseVector

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteHorizonResponseVector [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (n : Nat) (omega : Omega) : Feature -> Real

Source line 68 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonRidgeEstimate Compiled

Ridge least-squares estimate with deterministic positive-definite base.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonRidgeEstimate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteHorizonRidgeEstimate [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (n : Nat) (omega : Omega) : Feature -> Real

Source line 77 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonConfidenceThreshold Compiled

The squared self-normalized radius from the common-`R` Markov tail.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonConfidenceThreshold

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteHorizonConfidenceThreshold [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (feature : Nat -> Omega -> Feature -> Real) (R delta : Real) (n : Nat) (omega : Omega) : Real

Source line 87 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonConfidenceRadius Compiled

Confidence radius with an explicit deterministic regularization-bias cap.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonConfidenceRadius

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def finiteHorizonConfidenceRadius [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (feature : Nat -> Omega -> Feature -> Real) (R delta biasRadius : Real) (n : Nat) (omega : Omega) : Real

Source line 100 Chapter context: OFUL

theorem BanditRLProof.OFUL.one_le_det_add_posSemidef_div_det Compiled

Adding a positive-semidefinite Gram to a positive-definite base cannot reduce the determinant ratio below one.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.one_le_det_add_posSemidef_div_det

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem one_le_det_add_posSemidef_div_det [Fintype Feature] [DecidableEq Feature] (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (hG : G.PosSemidef) : 1 <= Matrix.det (V0 + G) / Matrix.det V0

Source line 113 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonConfidenceThreshold_nonneg Compiled

The squared confidence threshold is nonnegative for `0 < delta <= 1`.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonConfidenceThreshold_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem finiteHorizonConfidenceThreshold_nonneg [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (feature : Nat -> Omega -> Feature -> Real) (R delta : Real) (n : Nat) (omega : Omega) (hdelta : 0 < delta) (hdelta_one : delta <= 1) : 0 <= finiteHorizonConfidenceThreshold V0 feature R delta n omega

Source line 130 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonResponseVector_eq_featureGram_mulVec_add_noiseScore Compiled

Under the linear observation model, the response sufficient statistic is the feature Gram applied to the true parameter plus the martingale-noise score.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonResponseVector_eq_featureGram_mulVec_add_noiseScore

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem finiteHorizonResponseVector_eq_featureGram_mulVec_add_noiseScore [Fintype Feature] (thetaStar : Feature -> Real) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (n : Nat) (omega : Omega) (hresponse : forall i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) : finiteHorizonResponseVector feature response n omega = (finiteHorizonFeatureGram feature n omega).mulVec thetaStar + WithLp.ofLp (finiteHorizonNoiseScore feature noise n omega)

Source line 162 Chapter context: OFUL

theorem BanditRLProof.OFUL.posDef_nonsingInv_mulVec_mulVec Compiled

Applying the nonsingular inverse of a positive-definite matrix cancels it.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.posDef_nonsingInv_mulVec_mulVec

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem posDef_nonsingInv_mulVec_mulVec [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x : Feature -> Real) : A⁻¹.mulVec (A.mulVec x) = x

Source line 197 Chapter context: OFUL

theorem BanditRLProof.OFUL.posDef_mulVec_nonsingInv_mulVec Compiled

A positive-definite matrix also cancels its inverse on the left.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.posDef_mulVec_nonsingInv_mulVec

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem posDef_mulVec_nonsingInv_mulVec [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x : Feature -> Real) : A.mulVec (A⁻¹.mulVec x) = x

Source line 207 Chapter context: OFUL

theorem BanditRLProof.OFUL.matrixNorm_nonsingInv_mulVec_sq Compiled

The squared `A`-norm of `A⁻¹x` is the inverse quadratic form of `x`.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.matrixNorm_nonsingInv_mulVec_sq

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem matrixNorm_nonsingInv_mulVec_sq [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : A.PosDef) (x : Feature -> Real) : matrixNorm A (A⁻¹.mulVec x) ^ 2 = x ⬝ᵥ A⁻¹.mulVec x

Source line 219 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonRidgeEstimate_sub_eq_inverseScore_sub_inverseBias Compiled

Exact ridge-estimation error decomposition into inverse-Gram noise score and inverse-Gram regularization bias.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonRidgeEstimate_sub_eq_inverseScore_sub_inverseBias

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem finiteHorizonRidgeEstimate_sub_eq_inverseScore_sub_inverseBias [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (thetaStar : Feature -> Real) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (n : Nat) (omega : Omega) (hresponse : forall i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) : finiteHorizonRidgeEstimate V0 feature response n omega - thetaStar = (V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (WithLp.ofLp (finiteHorizonNoiseScore feature noise n omega)) - (V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (V0.mulVec thetaStar)

Source line 232 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonRidgeEstimate_error_matrixNorm_le_score_add_bias Compiled

Deterministic confidence decomposition: estimator error is bounded by the self-normalized score plus the regularization-bias norm.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonRidgeEstimate_error_matrixNorm_le_score_add_bias

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem finiteHorizonRidgeEstimate_error_matrixNorm_le_score_add_bias [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (thetaStar : Feature -> Real) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (n : Nat) (omega : Omega) (hresponse : forall i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) : matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate V0 feature response n omega - thetaStar) <= matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) ((V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (WithLp.ofLp (finiteHorizonNoiseScore feature noise n omega))) + matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) ((V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (V0.mulVec thetaStar))

Source line 294 Chapter context: OFUL

theorem BanditRLProof.OFUL.selfNormalizedQuadratic_gt_of_ridgeEstimate_error_matrixNorm_gt_confidenceRadius Compiled

Pointwise transport from confidence-ellipsoid failure to the compiled self-normalized score bad event.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.selfNormalizedQuadratic_gt_of_ridgeEstimate_error_matrixNorm_gt_confidenceRadius

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfNormalizedQuadratic_gt_of_ridgeEstimate_error_matrixNorm_gt_confidenceRadius [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (thetaStar : Feature -> Real) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (R delta biasRadius : Real) (n : Nat) (omega : Omega) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (hresponse : forall i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (hbias : matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) ((V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (V0.mulVec thetaStar)) <= biasRadius) (hbad : matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate V0 feature response n omega - thetaStar) > finiteHorizonConfidenceRadius V0 feature R delta biasRadius n omega) : (finiteHorizonNoiseScore feature noise n omega) ⬝ᵥ (V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (finiteHorizonNoiseScore feature noise n omega) > finiteHorizonConfidenceThreshold V0 feature R delta n omega

Source line 325 Chapter context: OFUL

theorem BanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le Compiled

Finite-horizon OFUL least-squares confidence ellipsoid. With probability at least `1 - delta`, the ridge-estimation error lies in the current Gram norm inside the self-normalized radius plus the supplied regularization-bias cap.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (thetaStar : Feature -> Real) (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) (biasRadius : Real) (hresponse : forall omega i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (hbias : forall omega, matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) ((V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (V0.mulVec thetaStar)) <= biasRadius) : mu {omega | matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate V0 feature response n omega - thetaStar) > finiteHorizonConfidenceRadius V0 feature R delta biasRadius n omega} <= ENNReal.ofReal delta

Source line 401 Open teaching explanation Chapter context: OFUL