BanditAlgorithm.least_squares_confidence_ellipsoid

Proved

by Shuze Chen · Jul 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

(Confidence ellipsoid; L&S Theorem 20.5) With the setup above and rewards $X_{t+1} = \langle \theta_*, A_{t+1}\rangle + \eta_{t+1}$ , let

\hat\theta_t = V_t(\lambda)^{-1} \sum_{s=1}^t X_s A_s

be the $\lambda$ -regularized least-squares estimator ( $\lambda > 0$ ). For $\delta \in (0,1)$ , with probability at least $1 - \delta$ , simultaneously for all $t \in \mathbb{N}$ :

\|\hat\theta_t - \theta_*\|_{V_t(\lambda)} < \sqrt{\lambda}\,\|\theta_*\|_2 + \sqrt{2\log\frac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^d}},

where $\|v\|_M = \sqrt{v^\top M v}$ .

Preamble

import Mathlib.Probability.Moments.SubGaussian
import Mathlib.Probability.Martingale.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.Real.Sqrt
import Definitions.Def_SelfNormalizedProcess


open MeasureTheory ProbabilityTheory Matrix

Formal statement

theorem BanditAlgorithm.least_squares_confidence_ellipsoid
    {Ω : Type} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P]
    {d : ℕ} (ℱ : Filtration ℕ mΩ)
    (A : ℕ → Ω → Fin d → ℝ) (η : ℕ → Ω → ℝ) (X : ℕ → Ω → ℝ) (θs : Fin d → ℝ)
    (hA : ∀ t : ℕ, Measurable[ℱ t] (A (t + 1)))
    (hη : ∀ t : ℕ, Measurable[ℱ (t + 1)] (η (t + 1)))
    (hsg : ∀ t : ℕ, HasCondSubgaussianMGF (ℱ t) (ℱ.le t) (η (t + 1)) 1 P)
    (hX : ∀ (t : ℕ) (ω : Ω), X (t + 1) ω = θs ⬝ᵥ A (t + 1) ω + η (t + 1) ω)
    {lam : ℝ} (hlam : 0 < lam) {δ : ℝ} (hδ : δ ∈ Set.Ioo (0 : ℝ) 1) :
    1 - δ ≤ P.real {ω | ∀ t : ℕ,
        Real.sqrt ((regularizedLeastSquares d lam A X t ω - θs) ⬝ᵥ
            regularizedDesignMatrix d lam A t ω *ᵥ
              (regularizedLeastSquares d lam A X t ω - θs))
          < Real.sqrt lam * Real.sqrt (θs ⬝ᵥ θs)
            + Real.sqrt (2 * Real.log (1 / δ)
                + Real.log ((regularizedDesignMatrix d lam A t ω).det / lam ^ d))} := by
  sorry

Source

L&S Theorem 20.5, p.260

Read-back

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

Setup and notation. Let $(\Omega, \mathcal{G}, P)$ be a probability space with $\Omega$ standard Borel, filtration $(\mathcal{F}_t)_{t\in\mathbb{N}}$ , dimension $d \in \mathbb{N}$ (no positivity assumed), actions $A_t : \Omega \to \mathbb{R}^d$ , noise $\eta_t : \Omega \to \mathbb{R}$ , responses $X_t : \Omega \to \mathbb{R}$ , and a fixed parameter vector $\theta_* \in \mathbb{R}^d$ . Define pointwise

V_t(\lambda) = \lambda I_d + \sum_{s=1}^{t} A_s A_s^{\top}, \qquad \hat\theta_t = V_t(\lambda)^{-1} \sum_{s=1}^{t} X_s A_s,

and write $\|v\| = \sqrt{\langle v, v\rangle}$ for the Euclidean norm.

Assertion. For $\lambda > 0$ and $\delta \in (0,1)$ ,

1 - \delta \;\le\; P\Bigl(\Bigl\{\,\omega \;\Bigm|\; \forall t \in \mathbb{N}:\;\; \sqrt{(\hat\theta_t - \theta_*)^{\top}\, V_t(\lambda)\, (\hat\theta_t - \theta_*)} \;<\; \sqrt{\lambda}\,\|\theta_*\| \;+\; \sqrt{\,2\log\tfrac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^{d}}\,}\,\Bigr\}\Bigr),

the probability being expressed as a real number, all quantities inside evaluated at $\omega$ .

Hypotheses.

Predictability: $A_{t+1}$ is $\mathcal{F}_t$ -measurable for every $t \ge 0$ ; adaptedness: $\eta_{t+1}$ is $\mathcal{F}_{t+1}$ -measurable for every $t \ge 0$ .
Conditional $1$ -sub-Gaussian noise: for every $t \ge 0$ and every $u \in \mathbb{R}$ , $P$ -almost surely $\mathbb{E}[e^{u\,\eta_{t+1}} \mid \mathcal{F}_t] \le e^{u^2/2}$ (via the regular conditional distribution given $\mathcal{F}_t$ , with the requisite integrability); variance proxy fixed to $1$ .
Exact linear model, pointwise: for every $t \ge 0$ and every $\omega \in \Omega$ (not merely a.s.), $X_{t+1}(\omega) = \langle \theta_*, A_{t+1}(\omega)\rangle + \eta_{t+1}(\omega)$ .
$\lambda > 0$ (strict), $\delta \in (0,1)$ (open).
$\Omega$ standard Borel, $P$ a probability measure.

Edge cases.

The inequality inside the event is strict ( $<$ ), and it must hold simultaneously for all $t \in \mathbb{N}$ , including $t = 0$ , where $\hat\theta_0 = 0$ and the left side equals $\sqrt{\lambda}\,\|\theta_*\|$ — strictly below the right side since $2\log(1/\delta) > 0$ .
Since $\lambda > 0$ , every $V_t(\lambda)$ is positive definite: the inverse in $\hat\theta_t$ is genuine, the quadratic form under the left square root is nonnegative, and $\det V_t(\lambda)/\lambda^d > 0$ .
Real square roots of negative arguments would be $0$ by convention; under the stated hypotheses all radicands here are nonnegative.
No boundedness is assumed on actions, on $\theta_*$ , or on the responses; $d = 0$ is admitted.
The claim is a lower bound $1 - \delta$ on the probability of the good event (not an equality).

Human review

Endorsed by Community (Bot) · Jul 29, 2026
Endorsed by Shuze Chen · Jul 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph