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.

The elliptical-potential bound for ridge design matrices

Statement

Let $d, n \geq 1$ , let $λ > 0$ , let $V_{0} = λ I_{d}$ , and let $a_{1}, \dots, a_{n} \in R^{d}$ . Define $V_{t} = V_{t - 1} + a_{t} a_{t}^{T}$ and $u_{t} = a_{t}^{T} V_{t - 1}^{- 1} a_{t}$ for $1 \leq t \leq n$ . Then every $V_{t}$ is positive definite, $u_{t} \geq 0$ , and

$\det V_{t} = \det V_{t - 1} (1 + u_{t}) (1 \leq t \leq n), \sum_{t = 1}^{n} \min {1, u_{t}} \leq 2 \log ⁣ (\frac{\det V_{n}}{\det V_{0}}) .$

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$ , a real $λ > 0$ , and vectors $a_{1}, \dots, a_{n} \in R^{d}$ .

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: $x^{T} y = ⟨ x, y ⟩$ and $x^{T} M x = ⟨ x, M x ⟩$ in standard coordinates.

[F2]

Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal and A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique: a real symmetric positive-definite matrix $V$ factors as $V = L L^{T}$ with $L$ lower triangular and positive diagonal.

[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)$ , For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , and The determinant of a triangular matrix is the product of its diagonal entries: determinant is defined by the Leibniz formula, is multiplicative, is unchanged by transpose, and for triangular $L$ equals the product of its diagonal entries.

[F4]

For $A \in M_{n} (R)$ and columns $u, v$ over a commutative ring, $\det (A + u v^{T}) = \det (A) + v^{T} adj (A) u$ : $\det (V + u v^{T}) = \det (V) + v^{T} adj (V) u$ .

[F5]

For every positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ : $V adj (V) = \det (V) I$ .

[F6]

A finite square real matrix is invertible if and only if its determinant is nonzero: a real square matrix with nonzero determinant is invertible.

[F7]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t and If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : for $x \geq 0$ , $\log (1 + x) = \int_{1}^{1 + x} d s / s$ , and pointwise inequalities between integrable functions on an increasing interval give the corresponding integral inequality.

[F8]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log (x y) = \log x + \log y$ for positive $x, y$ .

Proof

1.1givenF1algebra

For every $t \geq 0$ and nonzero $x \in R^{d}$ , $x^{T} V_{t} x = λ ∥ x ∥_{2}^{2} + \sum_{s = 1}^{t} (a_{s}^{T} x)^{2} > 0.$ Each $V_{t}$ is symmetric, so it is positive definite.

1.2F7algebra

If $u = 0$ , then $\min {1, u} = 0 = 2 \log (1 + u)$ . If $u > 0$ , the interval $[1, 1 + u]$ is nondegenerate, so [F7] and $1 / s \geq 1 / (1 + u)$ on that interval give $\log (1 + u) \geq u / (1 + u)$ . If $0 < u \leq 1$ , then $u / (1 + u) \geq u / 2$ ; if $u \geq 1$ , then $u / (1 + u) \geq 1 / 2$ . Thus $\min {1, u} \leq 2 \log (1 + u)$ in every case.

2.1step 1.1F2F3F6

By [F2]–[F3], write $V_{t} = L_{t} L_{t}^{T}$ with positive diagonal. Then $\det V_{t} = (\det L_{t})^{2} = (\prod_{i = 1}^{d} (L_{t})_{i i})^{2} > 0$ , so [F6] makes $V_{t}$ invertible. In particular $u_{t}$ is defined.

3.1step 1.1step 2.1F1algebra

The inverse of a positive-definite matrix is positive definite: if $a_{t} \neq 0$ and $y = V_{t - 1}^{- 1} a_{t}$ , then $y \neq 0$ and $u_{t} = a_{t}^{T} V_{t - 1}^{- 1} a_{t} = y^{T} V_{t - 1} y > 0$ ; if $a_{t} = 0$ , then $u_{t} = 0$ . Thus $u_{t} \geq 0$ .

3.2step 2.1F4F5algebra

Apply [F4] with $u = v = a_{t}$ and $V = V_{t - 1}$ . Since [F5] and invertibility in step 2.1 give $adj (V_{t - 1}) = \det (V_{t - 1}) V_{t - 1}^{- 1}$ , the result is $\det V_{t} = \det V_{t - 1} (1 + u_{t})$ .

4.1step 2.1step 3.2F8algebra

Divide the update identities of step 3.2 by the positive determinants of step 2.1 and multiply them for $t = 1, \dots, n$ . This gives $\det V_{n} / \det V_{0} = \prod_{t = 1}^{n} (1 + u_{t})$ , hence $\log (\det V_{n} / \det V_{0}) = \sum_{t = 1}^{n} \log (1 + u_{t})$ by [F8].

5.1step 3.1step 4.1step 1.2algebra∎

Apply step 1.2 to each nonnegative $u_{t}$ from step 3.1 and sum. Step 4.1 identifies the sum of logarithms with $\log (\det V_{n} / \det V_{0})$ , proving the claimed bound.

Depends on

Used by

LinUCB has a log-determinant high-probability pseudo-regret bound Theorem

Dependency tree · two levels

76 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)