LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Trace control of the regularized design determinant

Statement

Let $d, n \geq 1$ , let $λ > 0$ , let $L \geq 0$ , and let $a_{1}, \dots, a_{n} \in R^{d}$ satisfy $∥ a_{t} ∥_{2} \leq L$ . Put $V_{t} = λ I_{d} + \sum_{s = 1}^{t} a_{s} a_{s}^{T}$ and $V_{0} = λ I_{d}$ , and define $tr (M) = \sum_{i = 1}^{d} M_{i i}$ . Then

$0 < \det V_{t} (0 \leq t \leq n), \log ⁣ (\frac{\det V_{n}}{\det V_{0}}) \leq d \log ⁣ (1 + \frac{n L^{2}}{d λ}) .$

Statement references

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, §19.3, Lemma 19.4

Abbasi-Yadkori, Pál, and Szepesvári, Lemma 4

Facts & Assumptions

Given: Positive integers $d, n$ , reals $λ > 0$ and $L \geq 0$ , and vectors $a_{t} \in R^{d}$ with $∥ a_{t} ∥_{2} \leq L$ .

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $∥ x ∥_{2}^{2} = x^{T} x$ and the standard inner product is positive definite.

[F2]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: every real symmetric matrix has an orthonormal eigenbasis.

[F3]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , and For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ : determinant is defined by the Leibniz formula, is multiplicative, and is unchanged by transpose; a diagonal determinant is the product of its diagonal entries by The determinant of a triangular matrix is the product of its diagonal entries.

[F4]

The arithmetic mean, geometric mean inequality: for positive reals $μ_{1}, \dots, μ_{d}$ , $\prod_{i} μ_{i} \leq (\frac{1}{d} \sum_{i} μ_{i})^{d}$ .

[F5]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the natural logarithm is strictly increasing on positive reals and $\log (x^{d}) = d \log x$ for $x > 0$ .

Proof

1.1givenF1F2algebrachoose

For every nonzero $x \in R^{d}$ , $x^{T} V_{n} x = λ ∥ x ∥_{2}^{2} + \sum_{t = 1}^{n} (a_{t}^{T} x)^{2} > 0.$ Thus $V_{n}$ is symmetric positive definite. By [F2], choose an orthogonal matrix $Q$ and positive eigenvalues $μ_{1}, \dots, μ_{d}$ with $V_{n} = Q diag (μ_{1}, \dots, μ_{d}) Q^{T}$ .

1.2givenF1F2F3algebra

For each $0 \leq t \leq n$ , $x^{T} V_{t} x = λ ∥ x ∥_{2}^{2} + \sum_{s = 1}^{t} (a_{s}^{T} x)^{2} > 0$ for every nonzero $x$ . Thus $V_{t}$ is symmetric positive definite. By [F2], write $V_{t} = Q_{t} diag (ν_{1}, \dots, ν_{d}) Q_{t}^{T}$ with $Q_{t}$ orthogonal; positive definiteness gives $ν_{i} > 0$ for each $i$ . By [F3], $\det (Q_{t}^{T}) = \det (Q_{t})$ and $\det (diag (ν_{1}, \dots, ν_{d})) = \prod_{i} ν_{i}$ . Since $Q_{t}^{T} Q_{t} = I_{d}$ , multiplicativity gives $\det (Q_{t})^{2} = 1$ , hence $\det V_{t} = \prod_{i} ν_{i} > 0$ .

2.1step 1.1F3algebra

Since $Q^{T} Q = I_{d}$ , [F3] gives $(\det Q)^{2} = 1$ . Applying [F3] to the diagonalization yields $\det V_{n} = (\det Q) (\prod_{i} μ_{i}) (\det Q^{T}) = \prod_{i} μ_{i} > 0$ . Also, expanding the diagonal entries of $Q diag (μ_{i}) Q^{T}$ gives $tr (V_{n}) = \sum_{j = 1}^{d} μ_{j} \sum_{i = 1}^{d} Q_{i j}^{2} = \sum_{j = 1}^{d} μ_{j},$ because each column of $Q$ has Euclidean norm one.

3.1givenstep 2.1F1F4algebra

By [F4] and step 2.1, $\det V_{n} = \prod_{i} μ_{i} \leq {(\frac{\sum_{i} μ_{i}}{d})}^{d} = {(\frac{tr (V_{n})}{d})}^{d} .$ The definition of $V_{n}$ gives $tr (V_{n}) = d λ + \sum_{t} ∥ a_{t} ∥_{2}^{2} \leq d λ + n L^{2}$ .

4.1givenF3step 3.1algebra

Since $V_{0} = λ I_{d}$ is diagonal, [F3] gives $\det V_{0} = λ^{d} > 0$ . Dividing step 3.1 by this positive number yields $\frac{\det V_{n}}{\det V_{0}} \leq {(1 + \frac{n L^{2}}{d λ})}^{d} .$

5.1step 2.1step 4.1step 1.2F5algebra∎

The two sides in step 4.1 are positive by steps 2.1 and 4.1. Applying the increasing natural logarithm and then [F5] gives the claimed bound.

Depends on

Used by

Dependency tree · two levels

66 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (standard reference, not scraped)
Yasin Abbasi-Yadkori, Dávid Pál, and Csaba Szepesvári, Online Least Squares Estimation with Self-Normalized Processes: An Application to Bandit Problems (standard reference, not scraped)