Lemma 11 — the potential bound $\sum_t u_t^\top V_t^{-1} u_t \le n \log(r^2 T/\varepsilon + 1)$

Proved

LogRegretOCO.FTAL.elliptical_potential

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

determinantlinear-algebraonline-convex-optimizationp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $u_1, \dots, u_T \in \mathbb{R}^n$ satisfy $\|u_t\| \le r$ for some $r > 0$ , let $\varepsilon > 0$ , and define

V_t = \sum_{\tau=1}^t u_\tau u_\tau^\top + \varepsilon I_n \qquad (t = 1, \dots, T).

Then

\sum_{t=1}^T u_t^\top V_t^{-1} u_t \le n \log\left(\frac{r^2 T}{\varepsilon} + 1\right).

Each $V_t$ includes the current vector $u_t$ . The bound controls the sum of squared lengths of the vectors measured in the metric of the accumulated matrix, and grows only logarithmically in $T$ ; in the analysis of Follow the Leader it bounds the second term of the regret decomposition (Claim 2 of the paper).

Formalization Note The paper prints $V_t = \sum_{\tau=1}^t u_t u_t^\top + \varepsilon I_n$ , a typo for $u_\tau u_\tau^\top$ (its proof uses $V_t - V_{t-1} = u_t u_t^\top$ ); the Lean uses $u_\tau$ . The hypothesis $\varepsilon > 0$ , implicit in the paper, is stated (at $\varepsilon = 0$ the matrix can be singular and $r^2T/\varepsilon$ is $0$ in Lean). Vectors are in EuclideanSpace ℝ (Fin n) so that $\|\cdot\|$ is the Euclidean norm; matrices act on their coordinate vectors (WithLp.ofLp), and $u_\tau u_\tau^\top$ is Matrix.vecMulVec.

Preamble

import Mathlib

Formal statement

namespace LogRegretOCO.FTAL
theorem elliptical_potential {n : ℕ} (u : ℕ → EuclideanSpace ℝ (Fin n)) (r ε : ℝ) (T : ℕ)
    (hr : 0 < r) (hε : 0 < ε) (hu : ∀ t ∈ Finset.Icc 1 T, ‖u t‖ ≤ r) :
    let V : ℕ → Matrix (Fin n) (Fin n) ℝ := fun t =>
      ∑ τ ∈ Finset.Icc 1 t, Matrix.vecMulVec (WithLp.ofLp (u τ)) (WithLp.ofLp (u τ))
        + ε • (1 : Matrix (Fin n) (Fin n) ℝ)
    ∑ t ∈ Finset.Icc 1 T, dotProduct (WithLp.ofLp (u t)) (Matrix.mulVec (V t)⁻¹ (WithLp.ofLp (u t)))
      ≤ n * Real.log (r ^ 2 * T / ε + 1) := by sorry
end LogRegretOCO.FTAL

Source

Hazan, Agarwal, Kale, Logarithmic regret algorithms for online convex optimization, Mach Learn 69 (2007), p. 190, Lemma 11 (Appendix 2)

Read-back

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

Setting. Let $n \in \mathbb{N}$ , let $u_t \in \mathbb{R}^n$ for $t \in \mathbb{N}$ (with the Euclidean norm), let $r, \varepsilon$ be real numbers, and let $T \in \mathbb{N}$ .

Hypotheses.

$r > 0$ and $\varepsilon > 0$ .
$\|u_t\| \le r$ for every $t \in \{1, \dots, T\}$ .

Matrices. For each $t \in \mathbb{N}$ , define the $n \times n$ matrix

V_t = \sum_{\tau=1}^{t} u_\tau u_\tau^\top + \varepsilon I_n .

Note that $V_t$ includes the current term $u_t u_t^\top$ . Since $\varepsilon > 0$ , every $V_t$ is symmetric positive definite, so $V_t^{-1}$ is the genuine inverse.

Conclusion.

\sum_{t=1}^{T} u_t^\top V_t^{-1} u_t \;\le\; n \,\log\!\Big(\frac{r^2 T}{\varepsilon} + 1\Big),

where $\log$ is the natural logarithm and $T$ and $n$ are treated as real numbers.

Degenerate cases.

$T = 0$ . The left side is an empty sum, and the right side is $n \log 1 = 0$ , so the statement is $0 \le 0$ .
$n = 0$ . Both sides are $0$ .
Zero vectors. Some or all of the $u_t$ may be $0$ ; those terms contribute $0$ to the left side.
Indices beyond $T$ . Values of $u_t$ for $t > T$ are unconstrained and do not enter the statement.

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 11 — the potential bound ∑tut⊤Vt−1ut≤nlog⁡(r2T/ε+1)\sum_t u_t^\top V_t^{-1} u_t \le n \log(r^2 T/\varepsilon + 1)∑t​ut⊤​Vt−1​ut​≤nlog(r2T/ε+1)

Lemma 11 — the potential bound $\sum_t u_t^\top V_t^{-1} u_t \le n \log(r^2 T/\varepsilon + 1)$