Lemma 11 — Σₜ uₜᵀVₜ⁻¹uₜ ≤ n log(r²T/ε + 1)

Proved

LogRegretOCO.ONS.elliptical_potential

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

elliptical-potentiallinear-algebraonline-learningp2o-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\Big(\frac{r^2T}{\varepsilon}+1\Big).

Applied with $u_t=\nabla_t$ , $V_t=A_t$ and $r=G$ , this bounds the potential in the regret bound of the Online Newton Step by $n\log(G^2T/\varepsilon+1)$ .

Formalization Note The paper prints $V_t=\sum_{\tau=1}^t u_t u_t^\top+\varepsilon I_n$ ; the summation index is a typo and the statement uses $u_\tau u_\tau^\top$ , as the proof does. The hypothesis $\varepsilon>0$ is added: the page leaves it implicit, and without it $V_t$ need not be invertible. Norms are Euclidean and $\log$ is the natural logarithm.

Preamble

import Mathlib
import Definitions.Def_LogRegretOCO_ONS_Basic

Formal statement

namespace LogRegretOCO.ONS

/-- Lemma 11 (Hazan–Agarwal–Kale 2007, p. 190). Let `u_1, …, u_T ∈ ℝⁿ` with `‖u_t‖ ≤ r` for some
`r > 0`, let `ε > 0`, and let `V_t = Σ_{τ=1}^t u_τ u_τᵀ + ε Iₙ`. Then
`Σ_{t=1}^T u_tᵀ V_t⁻¹ u_t ≤ n log(r²T/ε + 1)`. -/
theorem elliptical_potential {n : ℕ} (u : ℕ → EuclideanSpace ℝ (Fin n)) (r ε : ℝ)
    (hr : 0 < r) (hε : 0 < ε) (T : ℕ) (hu : ∀ t ∈ Finset.Icc 1 T, ‖u t‖ ≤ r) :
    ∑ t ∈ Finset.Icc 1 T, quadForm (regGram ε u t)⁻¹ (u t) ≤
      n * Real.log (r ^ 2 * T / ε + 1) := by sorry

end LogRegretOCO.ONS

Source

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

Read-back

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

Setting. Let $n\in\mathbb{N}$ and let $u=(u_0,u_1,\dots)$ be a sequence of vectors in Euclidean space $\mathbb{R}^n$ . 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\}$ .
Nothing is assumed about $u_0$ or about $u_t$ with $t>T$ . None of these enter the statement.

The matrices. For each $t$ , let

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

Since $\varepsilon>0$ , each $V_t$ is 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^2T}{\varepsilon}+1\Big).

Here $n$ and $T$ are treated as real numbers. The argument of the logarithm is at least $1$ .

Degenerate cases:

$T=0$ : the sum is empty and the right side is $n\log 1=0$ , so the claim is $0\le0$ .
$n=0$ : every quadratic form is $0$ and the right side is $0$ .
All $u_t=0$ : the left side is $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