Prove2Me

BanditAlgorithm.elliptical_potential_lemma

Proved

by Shuze Chen · Jul 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditslinear-algebrapotential

(Elliptical potential lemma) Let V0∈Rd×dV_0 \in \mathbb{R}^{d\times d} be positive definite and a1,…,an∈Rda_1,\dots,a_n \in \mathbb{R}^d with ∥at∥2≤L\|a_t\|_2 \le L for all t∈[n]t\in[n], and set Vt=V0+∑s≤tasas⊤V_t = V_0 + \sum_{s\le t}a_sa_s^\top. Then

∑t=1n(1∧∥at∥Vt−1−12)≤2log⁡det⁡Vndet⁡V0≤2dlog⁡tr V0+nL2d det⁡(V0)1/d\sum_{t=1}^n \big(1 \wedge \|a_t\|^2_{V_{t-1}^{-1}}\big) \le 2\log\frac{\det V_n}{\det V_0} \le 2d\log\frac{\mathrm{tr}\,V_0 + nL^2}{d\,\det(V_0)^{1/d}}

— both inequalities, as a conjunction. Purely deterministic.

Preamble
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Trace
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real


open Matrix
Formal statement
theorem BanditAlgorithm.elliptical_potential_lemma {d n : ℕ} (hd : 0 < d)
    {V₀ : Matrix (Fin d) (Fin d) ℝ} (hV₀ : V₀.PosDef)
    {L : ℝ} (a : ℕ → Fin d → ℝ)
    (ha : ∀ t ∈ Finset.range n, Real.sqrt (a (t + 1) ⬝ᵥ a (t + 1)) ≤ L) :
    ∑ t ∈ Finset.range n,
        min 1 (a (t + 1) ⬝ᵥ
          (V₀ + ∑ s ∈ Finset.range t,
            vecMulVec (a (s + 1)) (a (s + 1)))⁻¹ *ᵥ a (t + 1)) ≤
      2 * Real.log
        ((V₀ + ∑ s ∈ Finset.range n,
          vecMulVec (a (s + 1)) (a (s + 1))).det / V₀.det) ∧
    2 * Real.log
        ((V₀ + ∑ s ∈ Finset.range n,
          vecMulVec (a (s + 1)) (a (s + 1))).det / V₀.det) ≤
      2 * d * Real.log
        ((V₀.trace + n * L ^ 2) / (d * V₀.det ^ ((1 : ℝ) / d))) := by
  sorry
Source
L&S Lemma 19.4, p.243
Human review

  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 9, 2026

    Confirmed by the mission captain (proposal self-audit).

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph