Lemma 10 — $\det A_{t+1}=\prod_{\tau=1}^{t}(1+w_\tau^2)$

Proved

StochLinOpt.UpperBound.det_designMatrix_succ

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditslinear-algebralinear-banditsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $x_1,x_2,\dots\in\mathbb R^n$ be any sequence, $A_t=I+\sum_{\tau=1}^{t-1}x_\tau x_\tau^\top$ and $w_\tau=\sqrt{x_\tau^\top A_\tau^{-1}x_\tau}$ . Then for every $t\ge0$ ,

\det A_{t+1}=\prod_{\tau=1}^{t}\big(1+w_\tau^2\big).

This expresses the growth of the log-volume of the precision matrix $A_t$ through the widths of the chosen decisions; it is the first half of the potential argument behind Lemma 9.

Formalization Note The paper prints the factor as $(1+w_t^2)$ under $\prod_{\tau=1}^t$ ; the index is a typo and the proof gives $(1+w_\tau^2)$ , which is what is stated. The paper's "for every $t\le T$ " places no restriction, so the statement is for every $t$ , including $t=0$ (empty product, $A_1=I$ ).

Preamble

import Mathlib
import Definitions.Def_StochLinOpt_UpperBound_confidenceBall2
import Definitions.Def_StochLinOpt_UpperBound_analysisQuantities

open Matrix

Formal statement

namespace StochLinOpt.UpperBound

theorem det_designMatrix_succ {n : ℕ} (x : ℕ → Fin n → ℝ) (t : ℕ) :
    (designMatrix x (t + 1)).det = ∏ τ ∈ Finset.Icc 1 t, (1 + width x τ ^ 2) := by sorry

end StochLinOpt.UpperBound

Source

Dani, Hayes, Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008, PDF p. 8, Lemma 10

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $n \in \mathbb{N}$ , any sequence $x = (x_0, x_1, \dots)$ of vectors in $\mathbb{R}^n$ , and $t \in \mathbb{N}$ . There are no other hypotheses. The notation is $A_s = I_n + \sum_{1\le\tau<s} x_\tau x_\tau^\top$ and $w_\tau = \sqrt{x_\tau^\top A_\tau^{-1} x_\tau}$ .

Conclusion.

\det A_{t+1} = \prod_{\tau=1}^{t} \big(1 + w_\tau^2\big).

Degenerate cases.

$t = 0$ : both sides equal $1$ ( $\det I_n$ and the empty product).
$n = 0$ : the determinant of the empty matrix is $1$ , every $w_\tau = 0$ , and both sides are $1$ .
$x_0$ : it never appears.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 10 — det⁡At+1=∏τ=1t(1+wτ2)\det A_{t+1}=\prod_{\tau=1}^{t}(1+w_\tau^2)detAt+1​=∏τ=1t​(1+wτ2​)

Lemma 10 — $\det A_{t+1}=\prod_{\tau=1}^{t}(1+w_\tau^2)$