BanditRLProof.OFULEllipticalPotential

Rank-one Gram matrix generated by one feature vector.

def rankOneGram {Feature : Type u} (x : Feature -> Real) : Matrix Feature Feature Real

The local rank-one Gram matrix is Mathlib's column-row product shape.

theorem rankOneGram_eq_replicateCol_mul_replicateRow {Feature : Type u} [Fintype Feature] (x : Feature -> Real) : rankOneGram x = Matrix.replicateCol Unit x * Matrix.replicateRow Unit x

Rank-one Gram matrices are Hermitian.

theorem rankOneGram_isHermitian {Feature : Type u} [Fintype Feature] (x : Feature -> Real) : (rankOneGram x).IsHermitian

Rank-one determinant lemma at the identity, specialized to feature Gram updates.

theorem det_one_add_rankOneGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (x : Feature -> Real) : (1 + rankOneGram x).det = 1 + dotProduct x x

The one-dimensional determinant factor in the rank-one matrix determinant lemma is the scalar `1 + x^T A^{-1} x`.

theorem det_rankOne_update_factor_eq_one_add_dotProduct_inv_mulVec {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (x : Feature -> Real) : (1 + Matrix.replicateRow Unit x * A⁻¹ * Matrix.replicateCol Unit x).det = 1 + dotProduct x (Matrix.mulVec (A⁻¹) x)

Rank-one matrix determinant lemma in OFUL feature notation. The invertibility side condition is kept as Mathlib's `IsUnit A.det`, matching the upstream Schur-complement API.

theorem det_add_rankOneGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (A : Matrix Feature Feature Real) (hA : IsUnit A.det) (x : Feature -> Real) : (A + rankOneGram x).det = A.det * (1 + dotProduct x (Matrix.mulVec (A⁻¹) x))

Determinant of the scalar regularization matrix `lambda I`.

theorem det_scalar_identity {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) : (Matrix.scalar Feature lambda : Matrix Feature Feature Real).det = lambda ^ Fintype.card Feature

Nonzero scalar regularization has nonzero determinant.

theorem det_scalar_identity_ne_zero {Feature : Type u} [Fintype Feature] [DecidableEq Feature] {lambda : Real} (hlambda : lambda ≠ 0) : (Matrix.scalar Feature lambda : Matrix Feature Feature Real).det ≠ 0

Nonzero scalar regularization satisfies Mathlib's determinant-unit side condition for the rank-one determinant update lemma.

theorem isUnit_det_scalar_identity {Feature : Type u} [Fintype Feature] [DecidableEq Feature] {lambda : Real} (hlambda : lambda ≠ 0) : IsUnit (Matrix.scalar Feature lambda : Matrix Feature Feature Real).det

First determinant update from the regularized scalar base `lambda I`. This is the one-step OFUL/LinUCB determinant recursion specialized to the empty-history base matrix. General log-det telescoping and determinant-growth bounds remain separate leaves.

theorem det_scalar_add_rankOneGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] {lambda : Real} (hlambda : lambda ≠ 0) (x : Feature -> Real) : ((Matrix.scalar Feature lambda : Matrix Feature Feature Real) + rankOneGram x).det = (Matrix.scalar Feature lambda : Matrix Feature Feature Real).det * (1 + dotProduct x (Matrix.mulVec ((Matrix.scalar Feature lambda : Matrix Feature Feature Real)⁻¹) x))

Quadratic form associated with a finite real matrix.

noncomputable def quadraticForm {Feature : Type u} [Fintype Feature] (A : Matrix Feature Feature Real) (y : Feature -> Real) : Real

Quadratic forms distribute over matrix addition.

theorem quadraticForm_add {Feature : Type u} [Fintype Feature] (A B : Matrix Feature Feature Real) (y : Feature -> Real) : quadraticForm (A + B) y = quadraticForm A y + quadraticForm B y

The Mathlib dot-product/mulVec form agrees with the local quadratic form.

theorem dotProduct_mulVec_eq_quadraticForm {Feature : Type u} [Fintype Feature] (A : Matrix Feature Feature Real) (y : Feature -> Real) : dotProduct y (Matrix.mulVec A y) = quadraticForm A y

Quadratic form of the scalar regularization matrix `lambda I`.

theorem quadraticForm_scalar_identity {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (y : Feature -> Real) : quadraticForm (Matrix.scalar Feature lambda : Matrix Feature Feature Real) y = lambda * (Finset.univ : Finset Feature).sum (fun i => y i ^ 2)

A finite sum of coordinate squares is positive for a nonzero vector.

theorem sum_sq_pos_of_exists_ne_zero {Feature : Type u} [Fintype Feature] (y : Feature -> Real) (hy : ∃ i : Feature, y i ≠ 0) : 0 < (Finset.univ : Finset Feature).sum (fun i => y i ^ 2)

A nonzero vector has a nonzero coordinate.

theorem exists_coord_ne_zero_of_ne_zero {Feature : Type u} (y : Feature -> Real) (hy : y ≠ 0) : ∃ i : Feature, y i ≠ 0

Finite-history feature Gram matrix `sum_t x_t x_t^T`.

noncomputable def featureGram {Time : Type v} {Feature : Type u} [Fintype Time] (x : Time -> Feature -> Real) : Matrix Feature Feature Real

Finite-history feature Gram matrices are Hermitian.

theorem featureGram_isHermitian {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] (x : Time -> Feature -> Real) : (featureGram x).IsHermitian

Regularized finite-history Gram matrix `lambda I + sum_t x_t x_t^T`.

noncomputable def regularizedFeatureGram {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Time -> Feature -> Real) : Matrix Feature Feature Real

The named regularized Gram unfolds to scalar regularization plus Gram.

theorem regularizedFeatureGram_eq_scalar_add_featureGram {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Time -> Feature -> Real) : regularizedFeatureGram lambda x = Matrix.scalar Feature lambda + featureGram x

Regularized finite-history feature Gram matrices are Hermitian.

theorem regularizedFeatureGram_isHermitian {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Time -> Feature -> Real) : (regularizedFeatureGram lambda x).IsHermitian

Prefix Gram matrix `sum_{t < T} x_t x_t^T` for a Nat-indexed history.

noncomputable def prefixFeatureGram {Feature : Type u} (x : Nat -> Feature -> Real) (T : Nat) : Matrix Feature Feature Real

Regularized prefix Gram matrix `lambda I + sum_{t < T} x_t x_t^T`.

noncomputable def regularizedPrefixFeatureGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) : Matrix Feature Feature Real

Prefix Grams grow by one rank-one feature update.

theorem prefixFeatureGram_succ {Feature : Type u} (x : Nat -> Feature -> Real) (T : Nat) : prefixFeatureGram x (T + 1) = prefixFeatureGram x T + rankOneGram (x T)

Regularized prefix Grams grow by one rank-one feature update.

theorem regularizedPrefixFeatureGram_succ {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) : regularizedPrefixFeatureGram lambda x (T + 1) = regularizedPrefixFeatureGram lambda x T + rankOneGram (x T)

The zero-horizon prefix Gram is the zero matrix.

theorem prefixFeatureGram_zero {Feature : Type u} (x : Nat -> Feature -> Real) : prefixFeatureGram x 0 = 0

The zero-horizon regularized prefix Gram is the scalar base `lambda I`.

theorem regularizedPrefixFeatureGram_zero {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) : regularizedPrefixFeatureGram lambda x 0 = (Matrix.scalar Feature lambda : Matrix Feature Feature Real)

The zero-horizon regularized prefix Gram determinant is `lambda^d`.

theorem det_regularizedPrefixFeatureGram_zero {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) : (regularizedPrefixFeatureGram lambda x 0).det = lambda ^ Fintype.card Feature

Prefix Gram matrices are Hermitian.

theorem prefixFeatureGram_isHermitian {Feature : Type u} [Fintype Feature] (x : Nat -> Feature -> Real) (T : Nat) : (prefixFeatureGram x T).IsHermitian

Regularized prefix Gram matrices are Hermitian.

theorem regularizedPrefixFeatureGram_isHermitian {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda x T).IsHermitian

The trace of a rank-one Gram is the squared feature norm.

theorem trace_rankOneGram {Feature : Type u} [Fintype Feature] (x : Feature -> Real) : (rankOneGram x).trace = dotProduct x x

The trace of the scalar regularization matrix is `d * lambda`.

theorem trace_scalar_identity {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) : (Matrix.scalar Feature lambda : Matrix Feature Feature Real).trace = (Fintype.card Feature : Real) * lambda

Prefix Gram trace as the finite sum of squared feature norms.

theorem trace_prefixFeatureGram {Feature : Type u} [Fintype Feature] (x : Nat -> Feature -> Real) (T : Nat) : (prefixFeatureGram x T).trace = (Finset.range T).sum (fun t => dotProduct (x t) (x t))

Regularized prefix Gram trace as scalar base plus squared feature norms.

theorem trace_regularizedPrefixFeatureGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda x T).trace = (Fintype.card Feature : Real) * lambda + (Finset.range T).sum (fun t => dotProduct (x t) (x t))

If each feature vector has squared norm at most `L2`, the regularized prefix Gram trace is bounded by `d * lambda + T * L2`.

theorem trace_regularizedPrefixFeatureGram_le {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hbound : forall t : Nat, t < T -> dotProduct (x t) (x t) <= L2) : (regularizedPrefixFeatureGram lambda x T).trace <= (Fintype.card Feature : Real) * lambda + T * L2

Finite nonnegative product is bounded by the corresponding arithmetic mean power.

theorem finset_prod_le_pow_sum_div_card_of_nonneg {ι : Type v} (s : Finset ι) (hs : s.Nonempty) (z : ι -> Real) (hz : forall i : ι, i ∈ s -> 0 <= z i) : (s.prod z) <= ((s.sum z) / (s.card : Real)) ^ s.card

Fintype specialization of the finite AM-GM product bound.

theorem prod_univ_le_pow_sum_div_card_of_nonneg {ι : Type v} [Fintype ι] [Nonempty ι] (z : ι -> Real) (hz : forall i : ι, 0 <= z i) : (Finset.univ.prod z) <= ((Finset.univ.sum z) / (Fintype.card ι : Real)) ^ Fintype.card ι

Positive-semidefinite determinant upper bound from AM-GM on eigenvalues.

theorem det_posSemidef_le_pow_trace_div_card {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (A : Matrix Feature Feature Real) (hA : A.PosSemidef) : A.det <= (A.trace / (Fintype.card Feature : Real)) ^ Fintype.card Feature

If a separate AM-GM/eigenvalue route supplies `det(V_T) <= (trace(V_T) / d)^d`, the prefix trace bound converts it into a dimension/radius determinant upper bound.

theorem det_regularizedPrefixFeatureGram_le_pow_trace_bound_average {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hdet_by_trace : (regularizedPrefixFeatureGram lambda x T).det <= ((regularizedPrefixFeatureGram lambda x T).trace / (Fintype.card Feature : Real)) ^ Fintype.card Feature) (havg_nonneg : 0 <= (regularizedPrefixFeatureGram lambda x T).trace / (Fintype.card Feature : Real)) (hbound : forall t : Nat, t < T -> dotProduct (x t) (x t) <= L2) : (regularizedPrefixFeatureGram lambda x T).det <= (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature

The quadratic form of a rank-one Gram matrix is the square of the projection of the query vector onto the feature vector.

theorem rankOneGram_quadraticForm_eq_sq {Feature : Type u} [Fintype Feature] (x y : Feature -> Real) : quadraticForm (rankOneGram x) y = ((Finset.univ : Finset Feature).sum (fun i => x i * y i)) ^ 2

Rank-one Gram matrices are Mathlib-positive semidefinite.

theorem rankOneGram_posSemidef {Feature : Type u} [Fintype Feature] (x : Feature -> Real) : (rankOneGram x).PosSemidef

Rank-one Gram matrices have nonnegative quadratic forms.

theorem rankOneGram_quadraticForm_nonneg {Feature : Type u} [Fintype Feature] (x y : Feature -> Real) : 0 <= quadraticForm (rankOneGram x) y

The quadratic form of a finite-history Gram matrix is a finite sum of squared feature projections.

theorem featureGram_quadraticForm_eq_sum_sq {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] (x : Time -> Feature -> Real) (y : Feature -> Real) : quadraticForm (featureGram x) y = (Finset.univ : Finset Time).sum (fun t => ((Finset.univ : Finset Feature).sum (fun i => x t i * y i)) ^ 2)

The quadratic form of a Nat-prefix Gram matrix is a finite range sum of squared feature projections.

theorem prefixFeatureGram_quadraticForm_eq_sum_sq {Feature : Type u} [Fintype Feature] (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) : quadraticForm (prefixFeatureGram x T) y = (Finset.range T).sum (fun t => ((Finset.univ : Finset Feature).sum (fun i => x t i * y i)) ^ 2)

The regularized Gram quadratic form is the scalar regularization term plus the finite-history Gram sum of squared feature projections.

theorem regularizedFeatureGram_quadraticForm_eq_sum_sq {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Time -> Feature -> Real) (y : Feature -> Real) : quadraticForm (regularizedFeatureGram lambda x) y = lambda * (Finset.univ : Finset Feature).sum (fun i => y i ^ 2) + (Finset.univ : Finset Time).sum (fun t => ((Finset.univ : Finset Feature).sum (fun i => x t i * y i)) ^ 2)

The regularized prefix Gram quadratic form is the scalar regularization term plus the prefix sum of squared feature projections.

theorem regularizedPrefixFeatureGram_quadraticForm_eq_sum_sq {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) : quadraticForm (regularizedPrefixFeatureGram lambda x T) y = lambda * (Finset.univ : Finset Feature).sum (fun i => y i ^ 2) + (Finset.range T).sum (fun t => ((Finset.univ : Finset Feature).sum (fun i => x t i * y i)) ^ 2)

Finite-history Gram matrices have nonnegative quadratic forms.

theorem featureGram_quadraticForm_nonneg {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] (x : Time -> Feature -> Real) (y : Feature -> Real) : 0 <= quadraticForm (featureGram x) y

Nat-prefix Gram matrices have nonnegative quadratic forms.

theorem prefixFeatureGram_quadraticForm_nonneg {Feature : Type u} [Fintype Feature] (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) : 0 <= quadraticForm (prefixFeatureGram x T) y

Regularized finite-history Gram matrices are PSD when `0 <= lambda`.

theorem regularizedFeatureGram_quadraticForm_nonneg {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 <= lambda) (x : Time -> Feature -> Real) (y : Feature -> Real) : 0 <= quadraticForm (regularizedFeatureGram lambda x) y

Regularized Nat-prefix Gram matrices are PSD when `0 <= lambda`.

theorem regularizedPrefixFeatureGram_quadraticForm_nonneg {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 <= lambda) (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) : 0 <= quadraticForm (regularizedPrefixFeatureGram lambda x T) y

Regularized finite-history Gram matrices have strictly positive quadratic forms on nonzero vectors when `0 < lambda`.

theorem regularizedFeatureGram_quadraticForm_pos_of_pos_lambda {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Time -> Feature -> Real) (y : Feature -> Real) (hy : ∃ i : Feature, y i ≠ 0) : 0 < quadraticForm (regularizedFeatureGram lambda x) y

Regularized Nat-prefix Gram matrices have strictly positive quadratic forms on nonzero vectors when `0 < lambda`.

theorem regularizedPrefixFeatureGram_quadraticForm_pos_of_pos_lambda {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) (hy : ∃ i : Feature, y i ≠ 0) : 0 < quadraticForm (regularizedPrefixFeatureGram lambda x T) y

Regularized finite-history Gram matrices are Mathlib-positive definite.

theorem regularizedFeatureGram_posDef {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Time -> Feature -> Real) : (regularizedFeatureGram lambda x).PosDef

Regularized Nat-prefix Gram matrices are Mathlib-positive definite.

theorem regularizedPrefixFeatureGram_posDef {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda x T).PosDef

Regularized Nat-prefix Gram determinant is bounded by trace average power.

theorem det_regularizedPrefixFeatureGram_le_pow_trace_div_card {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda x T).det <= ((regularizedPrefixFeatureGram lambda x T).trace / (Fintype.card Feature : Real)) ^ Fintype.card Feature

Concrete trace/radius determinant upper bound for regularized Nat-prefix Grams.

theorem det_regularizedPrefixFeatureGram_le_pow_trace_bound_average_of_pos_lambda {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hbound : forall t : Nat, t < T -> dotProduct (x t) (x t) <= L2) : (regularizedPrefixFeatureGram lambda x T).det <= (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature

Inverses of regularized Nat-prefix Gram matrices are positive definite.

theorem regularizedPrefixFeatureGram_inv_posDef {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : ((regularizedPrefixFeatureGram lambda x T)⁻¹).PosDef

Inverse-quadratic scalars of regularized Nat-prefix Gram matrices are nonnegative.

theorem regularizedPrefixFeatureGram_inv_quadratic_nonneg {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) (y : Feature -> Real) : 0 <= dotProduct y (Matrix.mulVec ((regularizedPrefixFeatureGram lambda x T)⁻¹) y)

Regularized finite-history Gram matrices have positive determinant.

theorem regularizedFeatureGram_det_pos {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Time -> Feature -> Real) : 0 < (regularizedFeatureGram lambda x).det

Regularized Nat-prefix Gram matrices have positive determinant.

theorem regularizedPrefixFeatureGram_det_pos {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : 0 < (regularizedPrefixFeatureGram lambda x T).det

Regularized finite-history Gram matrices have nonzero determinant.

theorem regularizedFeatureGram_det_ne_zero {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Time -> Feature -> Real) : (regularizedFeatureGram lambda x).det ≠ 0

Regularized Nat-prefix Gram matrices have nonzero determinant.

theorem regularizedPrefixFeatureGram_det_ne_zero {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda x T).det ≠ 0

Positive regularization supplies Mathlib's determinant-unit side condition for arbitrary finite-history regularized Gram matrices.

theorem isUnit_det_regularizedFeatureGram {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Time -> Feature -> Real) : IsUnit (regularizedFeatureGram lambda x).det

Positive regularization supplies Mathlib's determinant-unit side condition for Nat-prefix regularized Gram matrices.

theorem isUnit_det_regularizedPrefixFeatureGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (x : Nat -> Feature -> Real) (T : Nat) : IsUnit (regularizedPrefixFeatureGram lambda x T).det

One-step determinant recursion for an arbitrary finite-history regularized Gram matrix. This is the determinant identity consumed by OFUL/LinUCB log-det telescoping: the `IsUnit det` side condition is discharged from positive regularization.

theorem det_regularizedFeatureGram_add_rankOneGram {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : (regularizedFeatureGram lambda history + rankOneGram x).det = (regularizedFeatureGram lambda history).det * (1 + dotProduct x (Matrix.mulVec ((regularizedFeatureGram lambda history)⁻¹) x))

One-step determinant recursion for Nat-prefix regularized Gram matrices. This keeps the growing-history surface in a single Nat-indexed feature stream.

theorem det_regularizedPrefixFeatureGram_add_rankOneGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : (regularizedPrefixFeatureGram lambda history T + rankOneGram x).det = (regularizedPrefixFeatureGram lambda history T).det * (1 + dotProduct x (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) x))

Positive regularized Grams stay positive definite after a rank-one update.

theorem regularizedFeatureGram_add_rankOneGram_posDef {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : (regularizedFeatureGram lambda history + rankOneGram x).PosDef

Positive regularized prefix Grams stay positive definite after a rank-one update.

theorem regularizedPrefixFeatureGram_add_rankOneGram_posDef {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : (regularizedPrefixFeatureGram lambda history T + rankOneGram x).PosDef

The determinant after a positive regularized rank-one update is positive.

theorem det_regularizedFeatureGram_add_rankOneGram_pos {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : 0 < (regularizedFeatureGram lambda history + rankOneGram x).det

The determinant after a positive regularized prefix rank-one update is positive.

theorem det_regularizedPrefixFeatureGram_add_rankOneGram_pos {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : 0 < (regularizedPrefixFeatureGram lambda history T + rankOneGram x).det

The scalar rank-one determinant-update factor is positive.

theorem regularizedFeatureGram_rankOne_update_factor_pos {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : 0 < 1 + dotProduct x (Matrix.mulVec ((regularizedFeatureGram lambda history)⁻¹) x)

The scalar Nat-prefix rank-one determinant-update factor is positive.

theorem regularizedPrefixFeatureGram_rankOne_update_factor_pos {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : 0 < 1 + dotProduct x (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) x)

Logarithmic one-step determinant recursion for regularized Grams.

theorem log_det_regularizedFeatureGram_add_rankOneGram {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : Real.log (regularizedFeatureGram lambda history + rankOneGram x).det = Real.log (regularizedFeatureGram lambda history).det + Real.log (1 + dotProduct x (Matrix.mulVec ((regularizedFeatureGram lambda history)⁻¹) x))

Logarithmic one-step determinant recursion for regularized prefix Grams.

theorem log_det_regularizedPrefixFeatureGram_add_rankOneGram {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : Real.log (regularizedPrefixFeatureGram lambda history T + rankOneGram x).det = Real.log (regularizedPrefixFeatureGram lambda history T).det + Real.log (1 + dotProduct x (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) x))

Increment form of the logarithmic determinant recursion.

theorem log_det_regularizedFeatureGram_add_rankOneGram_sub {Time : Type v} {Feature : Type u} [Fintype Time] [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Time -> Feature -> Real) (x : Feature -> Real) : Real.log (regularizedFeatureGram lambda history + rankOneGram x).det - Real.log (regularizedFeatureGram lambda history).det = Real.log (1 + dotProduct x (Matrix.mulVec ((regularizedFeatureGram lambda history)⁻¹) x))

Increment form of the logarithmic determinant recursion for prefix Grams.

theorem log_det_regularizedPrefixFeatureGram_add_rankOneGram_sub {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (x : Feature -> Real) : Real.log (regularizedPrefixFeatureGram lambda history T + rankOneGram x).det - Real.log (regularizedPrefixFeatureGram lambda history T).det = Real.log (1 + dotProduct x (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) x))

Determinant recursion for the concrete prefix update `T -> T + 1`.

theorem det_regularizedPrefixFeatureGram_succ {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) : (regularizedPrefixFeatureGram lambda history (T + 1)).det = (regularizedPrefixFeatureGram lambda history T).det * (1 + dotProduct (history T) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) (history T)))

Log-det increment recursion for the concrete prefix update `T -> T + 1`.

theorem log_det_regularizedPrefixFeatureGram_succ_sub {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) : Real.log (regularizedPrefixFeatureGram lambda history (T + 1)).det - Real.log (regularizedPrefixFeatureGram lambda history T).det = Real.log (1 + dotProduct (history T) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history T)⁻¹) (history T)))

Finite forward-difference telescope used by log-det recursions.

theorem sum_range_forward_difference (Phi : Nat -> Real) (T : Nat) : (Finset.range T).sum (fun t => Phi (t + 1) - Phi t) = Phi T - Phi 0

Abstract finite-horizon log-det telescope from one-step log-update factors. This packages the shape needed after instantiating `detSeq` with an OFUL regularized Gram determinant process and `factor` with the corresponding rank-one update factor.

theorem sum_range_log_update_factor_eq_log_det_ratio (detSeq factor : Nat -> Real) (T : Nat) (hstep : forall t : Nat, t < T -> Real.log (detSeq (t + 1)) - Real.log (detSeq t) = Real.log (factor t)) : (Finset.range T).sum (fun t => Real.log (factor t)) = Real.log (detSeq T) - Real.log (detSeq 0)

Lower bound for `log (1 + z)` used in elliptical-potential estimates.

theorem div_one_add_self_le_log_one_add {z : Real} (hz : 0 <= z) : z / (1 + z) <= Real.log (1 + z)

For `0 <= z <= 1`, `z` is bounded by twice the log update.

theorem self_le_two_log_one_add_of_le_one {z : Real} (hz0 : 0 <= z) (hz1 : z <= 1) : z <= 2 * Real.log (1 + z)

Numeric endpoint: `1 <= 2 * log 2`.

theorem one_le_two_log_two : (1 : Real) <= 2 * Real.log 2

Elliptical-potential scalar inequality: `min 1 z <= 2 log (1+z)`.

theorem min_one_le_two_log_one_add {z : Real} (hz : 0 <= z) : min 1 z <= 2 * Real.log (1 + z)

Finite-sum scalar elliptical-potential wrapper. This consumes nonnegativity of each update scalar and leaves the log telescope or determinant-ratio identity as a separate input.

theorem sum_range_min_one_le_two_sum_log_one_add (u : Nat -> Real) (T : Nat) (hu : forall t : Nat, t < T -> 0 <= u t) : (Finset.range T).sum (fun t => min 1 (u t)) <= 2 * (Finset.range T).sum (fun t => Real.log (1 + u t))

Clipped finite-sum upper-bound handoff under an explicit log-sum certificate. This is the scalar clipped counterpart of the later small-update raw-sum handoff and does not mention any determinant or matrix route.

theorem sum_range_min_one_le_two_of_sum_log_one_add_le (u : Nat -> Real) (T : Nat) (B : Real) (hu : forall t : Nat, t < T -> 0 <= u t) (hlog_sum_le : (Finset.range T).sum (fun t => Real.log (1 + u t)) <= B) : (Finset.range T).sum (fun t => min 1 (u t)) <= 2 * B

Raw finite-sum log upper bound under an explicit small-update contract. For nonnegative update scalars bounded by one, the unclipped sum agrees with the clipped sum consumed by the determinant-growth route.

theorem sum_range_le_two_sum_log_one_add_of_le_one (u : Nat -> Real) (T : Nat) (hu_nonneg : forall t : Nat, t < T -> 0 <= u t) (hu_le_one : forall t : Nat, t < T -> u t <= 1) : (Finset.range T).sum (fun t => u t) <= 2 * (Finset.range T).sum (fun t => Real.log (1 + u t))

Raw finite-sum upper-bound handoff under an explicit log-sum certificate. This keeps the scalar small-update proof independent from any determinant or matrix route that might later prove the log-sum upper bound.

theorem sum_range_le_two_of_sum_log_one_add_le_of_le_one (u : Nat -> Real) (T : Nat) (B : Real) (hu_nonneg : forall t : Nat, t < T -> 0 <= u t) (hu_le_one : forall t : Nat, t < T -> u t <= 1) (hlog_sum_le : (Finset.range T).sum (fun t => Real.log (1 + u t)) <= B) : (Finset.range T).sum (fun t => u t) <= 2 * B

Concrete finite-horizon log-det telescope for Nat-prefix regularized Grams. This is the growing-history instantiation of the abstract telescope. It does not prove any determinant-growth upper bound for the resulting ratio.

theorem sum_range_log_regularizedPrefixFeatureGram_update_factor_eq_log_det_ratio {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) : (Finset.range T).sum (fun t => Real.log (1 + dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) = Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (regularizedPrefixFeatureGram lambda history 0).det

Concrete prefix log-det telescope with the scalar-base determinant expanded as `lambda ^ d`.

theorem sum_range_log_regularizedPrefixFeatureGram_update_factor_eq_log_det_sub_base {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) : (Finset.range T).sum (fun t => Real.log (1 + dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) = Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature)

Concrete prefix determinant-growth consumer with the inverse-quadratic nonnegativity contract left explicit. This is the finite-sum elliptical-potential inequality once each update scalar `x_t^T V_t^{-1} x_t` is known nonnegative.

theorem sum_range_min_prefix_update_le_two_log_det_sub_base {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (hquad_nonneg : forall t : Nat, t < T -> 0 <= dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * (Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature))

Raw prefix inverse-quadratic sum bound from the terminal log-determinant ratio, with inverse-quadratic nonnegativity and small-update contracts left explicit.

theorem sum_range_prefix_update_le_two_log_det_sub_base {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (hquad_nonneg : forall t : Nat, t < T -> 0 <= dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * (Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature))

Concrete prefix determinant-growth consumer with inverse-quadratic nonnegativity discharged from the positive-definite inverse of the regularized Gram matrix.

theorem sum_range_min_prefix_update_le_two_log_det_sub_base_of_pos_lambda {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * (Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature))

Raw prefix inverse-quadratic sum bound from the terminal log-determinant ratio, under a small-update contract. When every update scalar is at most one, the raw update sum agrees with the clipped sum controlled by the log-det telescope endpoint.

theorem sum_range_prefix_update_le_two_log_det_sub_base_of_update_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * (Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature))

If a separate route supplies a terminal log-determinant upper bound, the clipped prefix inverse-quadratic sum inherits the corresponding bound.

theorem sum_range_min_prefix_update_le_two_log_det_upper {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (B : Real) (hlog_upper : Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature) <= B) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * B

Raw prefix inverse-quadratic sum bound from a terminal log-determinant upper bound, under a small-update contract. When every update scalar is at most one, the raw update sum agrees with the clipped sum consumed by the determinant-growth route.

theorem sum_range_prefix_update_le_two_log_det_upper_of_update_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (B : Real) (hlog_upper : Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature) <= B) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * B

A multiplicative determinant upper bound of the form `det(V_T) <= lambda^d * exp(B)` supplies the terminal log-determinant upper bound used by the clipped elliptical-potential consumer.

theorem log_det_regularizedPrefixFeatureGram_sub_base_le_of_det_le_mul_exp {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (B : Real) (hdet_upper : (regularizedPrefixFeatureGram lambda history T).det <= lambda ^ Fintype.card Feature * Real.exp B) : Real.log (regularizedPrefixFeatureGram lambda history T).det - Real.log (lambda ^ Fintype.card Feature) <= B

Clipped prefix inverse-quadratic sum bound from a multiplicative terminal determinant upper bound.

theorem sum_range_min_prefix_update_le_two_det_mul_exp_upper {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (B : Real) (hdet_upper : (regularizedPrefixFeatureGram lambda history T).det <= lambda ^ Fintype.card Feature * Real.exp B) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * B

Raw prefix inverse-quadratic sum bound from a multiplicative determinant upper bound, under a small-update contract.

theorem sum_range_prefix_update_le_two_det_mul_exp_upper_of_update_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (B : Real) (hdet_upper : (regularizedPrefixFeatureGram lambda history T).det <= lambda ^ Fintype.card Feature * Real.exp B) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * B

Scalar simplification for the AM-GM trace/radius determinant upper bound. With `d = Fintype.card Feature` and squared-radius bound `L2 >= 0`, the trace-average expression is bounded by the multiplicative exponential form with exponent `d * (T * L2 / (d * lambda))`.

theorem trace_average_pow_le_lambda_pow_mul_exp_dim_scaled {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp ((Fintype.card Feature : Real) * ((T * L2) / ((Fintype.card Feature : Real) * lambda)))

Scalar AM-GM trace/radius simplification in the standard logarithmic determinant-growth form. This keeps the textbook `d * log (1 + T L2 / (d lambda))` exponent instead of linearizing it by `log (1 + x) <= x`.

theorem trace_average_pow_le_lambda_pow_mul_exp_log {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda)))

Dimension cancellation in the scalar OFUL trace-average exponent.

theorem trace_average_exp_exponent_dim_cancel {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (T : Nat) (L2 : Real) : (Fintype.card Feature : Real) * ((T * L2) / ((Fintype.card Feature : Real) * lambda)) = (T * L2) / lambda

Scalar AM-GM trace/radius simplification with the dimension-cancelled exponent `T * L2 / lambda`.

theorem trace_average_pow_le_lambda_pow_mul_exp {Feature : Type u} [Fintype Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp ((T * L2) / lambda)

If the trace-average determinant upper bound is simplified to the standard multiplicative `lambda^d * exp(B)` form, regularized Nat-prefix Grams inherit that multiplicative determinant upper bound.

theorem det_regularizedPrefixFeatureGram_le_mul_exp_of_trace_average_bound {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 B : Real) (hbound : forall t : Nat, t < T -> dotProduct (history t) (history t) <= L2) (haverage_to_exp : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp B) : (regularizedPrefixFeatureGram lambda history T).det <= lambda ^ Fintype.card Feature * Real.exp B

Clipped prefix inverse-quadratic sum bound from the AM-GM determinant trace route plus a separate scalar simplification to `lambda^d * exp(B)`.

theorem sum_range_min_prefix_update_le_two_of_trace_average_bound {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 B : Real) (hbound : forall t : Nat, t < T -> dotProduct (history t) (history t) <= L2) (haverage_to_exp : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp B) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * B

Unclipped prefix inverse-quadratic sum bound from a scalar trace-average certificate, under a small-update contract. When each update scalar is at most one, the raw update sum agrees with the clipped sum used by the standard elliptical-potential route.

theorem sum_range_prefix_update_le_two_of_trace_average_bound_of_update_le_one {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 B : Real) (hbound : forall t : Nat, t < T -> dotProduct (history t) (history t) <= L2) (haverage_to_exp : (((Fintype.card Feature : Real) * lambda + T * L2) / (Fintype.card Feature : Real)) ^ Fintype.card Feature <= lambda ^ Fintype.card Feature * Real.exp B) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * B

Concrete determinant upper bound obtained by combining the AM-GM trace/radius route with the scalar exponential simplification.

theorem det_regularizedPrefixFeatureGram_le_mul_exp_trace_average_dim_scaled {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) * ((T * L2) / ((Fintype.card Feature : Real) * lambda)))

Concrete clipped elliptical-potential sum bound obtained from the trace/radius route and scalar exponential simplification.

theorem sum_range_min_prefix_update_le_two_trace_average_dim_scaled {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) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * ((Fintype.card Feature : Real) * ((T * L2) / ((Fintype.card Feature : Real) * lambda)))

Concrete raw small-update elliptical-potential sum bound with the dimension-scaled exponent `d * (T * L2 / (d * lambda))`.

theorem sum_range_prefix_update_le_two_trace_average_dim_scaled_of_update_le_one {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) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * ((Fintype.card Feature : Real) * ((T * L2) / ((Fintype.card Feature : Real) * lambda)))

Concrete determinant upper bound from trace/radius with the dimension-cancelled exponent `T * L2 / lambda`.

theorem det_regularizedPrefixFeatureGram_le_mul_exp_trace_average {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 ((T * L2) / lambda)

Concrete determinant upper bound from trace/radius with the standard logarithmic exponent `d * log (1 + T L2 / (d lambda))`.

theorem det_regularizedPrefixFeatureGram_le_mul_exp_trace_average_log {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)))

Concrete clipped elliptical-potential sum bound with the dimension-cancelled exponent `T * L2 / lambda`.

theorem sum_range_min_prefix_update_le_two_trace_average {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) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * ((T * L2) / lambda)

Concrete raw small-update elliptical-potential sum bound with the dimension-cancelled exponent `T * L2 / lambda`.

theorem sum_range_prefix_update_le_two_trace_average_of_update_le_one {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) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t))) <= 2 * ((T * L2) / lambda)

Concrete clipped elliptical-potential sum bound with the standard logarithmic trace/radius endpoint. This is the deterministic OFUL/LinUCB textbook shape before self-normalized concentration and confidence-ellipsoid arguments are introduced.

theorem sum_range_min_prefix_update_le_two_trace_average_log {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) : (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)))

Unclipped logarithmic elliptical-potential bound for small update scalars. If every inverse-quadratic update scalar is already at most one, the clipped sum bound applies to the raw update sum.

theorem sum_range_prefix_update_le_two_trace_average_log_of_update_le_one {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) (hupdate_le_one : forall t : Nat, t < T -> dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)) <= 1) : (Finset.range T).sum (fun t => 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)))