Lemma 9 (corrected) — $\sum_{\tau\le t}\min(w_\tau^2,1)\le2n\ln(t+1)$

Proved

StochLinOpt.UpperBound.sum_min_width_sq_le

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

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

Let $x_1,x_2,\dots\in[-1,1]^n$ , $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$ ,

\sum_{\tau=1}^{t}\min\big(w_\tau^2,1\big)\le2n\ln(t+1).

This is the elliptical potential bound: the sum of the squared widths cannot grow faster than logarithmically, which is what makes the regret sublinear.

Formalization Note The paper prints $2n\ln t$ ; its proof gives $2n\ln(t+1)$ (it bounds the sum by $2\ln\det A_{t+1}\le2n\ln(t+1)$ , using Lemma 11 at $t+1$ ). The printed bound is false at $t=1$ : the left side is $\min(w_1^2,1)>0$ when $x_1\ne0$ , while $2n\ln1=0$ . The corrected bound is stated. The hypothesis $x_\tau\in[-1,1]^n$ is the paper's standing Section 5 coordinate choice ( $D\subseteq[-1,1]^n$ ).

Preamble

import Mathlib
import Definitions.Def_StochLinOpt_UpperBound_confidenceBall2
import Definitions.Def_StochLinOpt_UpperBound_analysisQuantities

open Matrix

Formal statement

namespace StochLinOpt.UpperBound

theorem sum_min_width_sq_le {n : ℕ} (x : ℕ → Fin n → ℝ)
    (hx : ∀ τ : ℕ, 1 ≤ τ → ∀ i, |x τ i| ≤ 1) (t : ℕ) :
    ∑ τ ∈ Finset.Icc 1 t, min (width x τ ^ 2) 1 ≤ 2 * n * Real.log (t + 1) := by sorry

end StochLinOpt.UpperBound

Source

Dani, Hayes, Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008, PDF p. 8, Lemma 9 (with proof via Lemmas 10 and 11)

Read-back

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

Setting. $n \in \mathbb{N}$ and a sequence $x$ in $\mathbb{R}^n$ such that $|x_{\tau,i}| \le 1$ for every $\tau \ge 1$ and every coordinate $i$ ; $x_0$ is unconstrained. Let $t \in \mathbb{N}$ . The notation is $A_\tau = I + \sum_{1\le s<\tau} x_s x_s^\top$ and $w_\tau = \sqrt{x_\tau^\top A_\tau^{-1} x_\tau}$ .

Conclusion.

\sum_{\tau=1}^{t} \min\big(w_\tau^2,\ 1\big) \;\le\; 2\,n\,\ln(t+1).

Degenerate cases.

$t = 0$ : the claim is $0 \le 0$ .
$n = 0$ : every $w_\tau = 0$ , and the claim is $0 \le 0$ .

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 9 (corrected) — ∑τ≤tmin⁡(wτ2,1)≤2nln⁡(t+1)\sum_{\tau\le t}\min(w_\tau^2,1)\le2n\ln(t+1)∑τ≤t​min(wτ2​,1)≤2nln(t+1)

Lemma 9 (corrected) — $\sum_{\tau\le t}\min(w_\tau^2,1)\le2n\ln(t+1)$