BanditAlgorithm.linear_bandit_linucb_expected_regret

Proved

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

banditslinearregret

(Expected regret — Corollary 19.3) There is a universal constant $C > 0$ such that for every fixed finite action set $\mathrm{arms} : \mathrm{Fin}\,k \to \mathbb{R}^d$ with $\|\mathrm{arms}_j\|_2 \le L$ (with $L \ge 1$ , $n \ge 2$ ) there is a policy $\pi$ (LinUCB with $\delta = 1/n$ and $\beta_t$ from Eq. (19.8)/Theorem 20.5) such that for every linear bandit instance with

$\|\theta_*\|_2 \le 1$ (i.e. $m_2 = 1$ in Eq. (19.8)), and
$\sup_{a,b}\langle\theta_*,a-b\rangle \le 1$ (= Assumption 19.1(b)),

the expected regret satisfies

R_n \le C d\sqrt{n}\log(nL).

Preamble

import Definitions.Def_StochasticLinearBandit
import Definitions.Def_banditRegret


open Matrix MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.linear_bandit_linucb_expected_regret :
    ∃ C : ℝ, 0 < C ∧
      ∀ (d k n : ℕ) (L : ℝ), 0 < d → 0 < k → 2 ≤ n → 1 ≤ L →
        ∀ arms : Fin k → Fin d → ℝ,
          (∀ j, Real.sqrt (arms j ⬝ᵥ arms j) ≤ L) →
          ∃ π : BanditPolicy k,
            ∀ (θstar : Fin d → ℝ) (ν : StochasticBandit k),
              IsLinearBandit arms θstar ν →
              Real.sqrt (θstar ⬝ᵥ θstar) ≤ 1 →
              (∀ j j' : Fin k, θstar ⬝ᵥ (arms j - arms j') ≤ 1) →
              banditRegret ν π n ≤
                C * d * Real.sqrt n * Real.log (n * L) := by
  sorry

Source

L&S Corollary 19.3, p.243

Read-back

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

Setup and notation. This is an existence statement about $k$ -armed stochastic bandits with linear structure. A $k$ -armed bandit $\nu$ is a $k$ -tuple of probability measures $\nu_j$ on $\mathbb{R}$ with arm means $\mu_j = \int r \, d\nu_j(r)$ ; a policy $\pi$ is a family of Markov kernels selecting an arm from each history of arm–reward pairs; the interaction law $\mathbb{P}_{\nu,\pi,n}$ on length- $n$ histories draws at each round an arm from the policy kernel and then a reward from that arm's distribution; and the expected regret is

\mathfrak{R}_n(\nu, \pi) \;=\; n \cdot \max_{j} \mu_j \;-\; \mathbb{E}_{h\sim\mathbb{P}_{\nu,\pi,n}}\Bigl[\sum_{t=0}^{n-1} X_t\Bigr],

where $X_t$ is the recorded reward of round $t$ . For a feature map $\phi_j \in \mathbb{R}^d$ ( $j = 1,\dots,k$ ) and $\theta_* \in \mathbb{R}^d$ , say $\nu$ realizes $(\phi, \theta_*)$ iff $\mu_j = \langle \phi_j, \theta_*\rangle$ for every arm $j$ and $\nu$ is $1$ -sub-Gaussian (each $\nu_j$ integrable, and $\int e^{u(r-\mu_j)}\,d\nu_j(r) \le e^{u^2/2}$ for every $u \in \mathbb{R}$ , with the corresponding integrability).

Assertion.

\exists\, C > 0 \text{ such that } \forall\, d, k, n, L,\ \forall\, \phi,\ \exists\, \pi,\ \forall\, (\theta_*, \nu): \qquad \mathfrak{R}_n(\nu, \pi) \;\le\; C\, d\, \sqrt{n}\, \log(nL),

with the quantifiers and side conditions detailed below.

Hypotheses (in quantifier order).

A single constant $C > 0$ works for all instances.
$d \ge 1$ , $k \ge 1$ , $n \ge 2$ , and $L \ge 1$ (a real).
The features are bounded: $\|\phi_j\| = \sqrt{\langle \phi_j, \phi_j\rangle} \le L$ for every arm $j$ .
The policy $\pi$ is chosen after $(d, k, n, L, \phi)$ but before $(\theta_*, \nu)$ : one policy must satisfy the bound uniformly over every parameter/bandit pair meeting the remaining conditions.
$\nu$ realizes the linear bandit $(\phi, \theta_*)$ as above (linear means, $1$ -sub-Gaussian).
$\|\theta_*\| \le 1$ .
Bounded mean spread: $\langle \theta_*,\, \phi_j - \phi_{j'}\rangle \le 1$ for every ordered pair of arms $j, j'$ .

Edge cases.

The bound controls only the expected regret $\mathfrak{R}_n$ (a Bochner integral, $0$ by convention if non-integrable); it is not a high-probability statement.
The optimal mean is a supremum over the finitely many arms; with $k \ge 1$ it is a genuine maximum.
Under $n \ge 2$ and $L \ge 1$ , $\log(nL) \ge \log 2 > 0$ , so the right-hand side is positive.
The sub-Gaussian variance proxy is fixed at $1$ ; no other noise assumption appears.
Nothing constrains the policy to be computable or to have any specific algorithmic form — only existence is claimed.

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