BanditAlgorithm.bandit_asymptotically_optimal_ucb_regret_bound

Proved

by Shuze Chen · 1 vote · Jul 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

banditsregretucb

(Asymptotically optimal UCB, finite-time, GOAL) For any 1-subgaussian $k$ -armed bandit $\nu$ and any policy $\pi$ that is an instance of Algorithm 6 (index $\hat\mu_i(t-1) + \sqrt{\frac{2\log f(t)}{T_i(t-1)}}$ with $f(t) = 1 + t\log^2 t$ ), the regret satisfies

R_n \le \sum_{i:\Delta_i>0} \inf_{\varepsilon\in(0,\Delta_i)} \Delta_i\left(1 + \frac{5}{\varepsilon^2} + \frac{2\big(\log f(n) + \sqrt{\pi\log f(n)} + 1\big)}{(\Delta_i-\varepsilon)^2}\right).

The per-arm infimum inside the sum is encoded in the equivalent $\forall$ -family form: the bound holds at every family $\varepsilon : \mathrm{Fin}\ k \to \mathbb{R}$ with $\varepsilon_i \in (0, \Delta_i)$ for each suboptimal arm $i$ .

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_asymptoticUcbPolicy
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_asymptotically_optimal_ucb_regret_bound {k : ℕ}
    {ν : StochasticBandit k} (hν : IsSubgaussianBandit 1 ν)
    {π : BanditPolicy k} (hπ : IsAsymptoticUCBPolicy π) (n : ℕ)
    (ε : Fin k → ℝ)
    (hε : ∀ i, 0 < banditGap ν i → ε i ∈ Set.Ioo 0 (banditGap ν i)) :
    banditRegret ν π n ≤
      ∑ i ∈ Finset.univ.filter (fun i ↦ 0 < banditGap ν i),
        banditGap ν i *
          (1 + 5 / ε i ^ 2 +
            2 * (Real.log (asymptoticUcbSchedule n) +
                Real.sqrt (Real.pi * Real.log (asymptoticUcbSchedule n)) + 1) /
              (banditGap ν i - ε i) ^ 2) := by
  sorry

Source

L&S Theorem 8.1, Eq. (8.1), p.117

Read-back

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

Setup and notation. A $k$ -armed bandit $\nu$ is a family of Borel probability measures $(P_i)_{i<k}$ on $\mathbb{R}$ . Write $\mu_i=\int x\,dP_i(x)$ (a Bochner integral, equal to $0$ by convention if the identity is not $P_i$ -integrable), $\mu^{*}=\sup_{i<k}\mu_i$ (equal to $0$ when $k=0$ , by the real convention for suprema over an empty range), and $\Delta_i=\mu^{*}-\mu_i$ . A history of length $m$ is a function $t\mapsto (A_t,X_t)$ , $t<m$ , of arm/reward pairs; $T_i(h)$ is the number of rounds of $h$ playing arm $i$ and $\hat\mu_i(h)$ the corresponding empirical mean (with $x/0=0$ , so both are $0$ for unpulled arms). A policy $\pi$ is a family of Markov kernels $\pi_m(\cdot\mid h)$ from length- $m$ histories to distributions over arms. $\mathbb{P}^{n}_{\nu,\pi}$ denotes the canonical probability measure on length- $n$ histories, defined recursively: $\mathbb{P}^{0}$ is the point mass at the empty history, and $\mathbb{P}^{m+1}$ is the law of the history obtained by sampling $h\sim\mathbb{P}^{m}$ , then an arm $A_m\sim\pi_m(\cdot\mid h)$ , then a reward $X_m\sim P_{A_m}$ , and appending $(A_m,X_m)$ to $h$ . The expected regret is

R_n=n\,\mu^{*}-\int\Bigl(\sum_{t<n}X_t\Bigr)d\mathbb{P}^{n}_{\nu,\pi},

again a Bochner integral ( $0$ by convention if the total reward is not integrable, in which case $R_n=n\mu^{*}$ ). The schedule is $f(t)=1+t(\log t)^{2}$ with $\log 0=0$ (so $f(0)=f(1)=1$ ), and the index of arm $i$ at a length- $m$ history is $\gamma_i(h)=\hat\mu_i(h)+\sqrt{2\log f(m+1)/T_i(h)}$ . The policy property assumed of $\pi$ reads: for every $m$ and every length- $m$ history $h$ there is an arm $a$ with $\pi_m(\cdot\mid h)=\delta_a$ , such that if some arm is unpulled in $h$ then $a$ is unpulled, and if all arms have been pulled then $\gamma_j(h)\le\gamma_a(h)$ for every arm $j$ .

Assertion. For the given horizon $n$ and real family $(\varepsilon_i)_{i<k}$ ,

R_n\ \le\ \sum_{i:\,\Delta_i>0}\Delta_i\left(1+\frac{5}{\varepsilon_i^{2}}+\frac{2\bigl(\log f(n)+\sqrt{\pi\,\log f(n)}+1\bigr)}{(\Delta_i-\varepsilon_i)^{2}}\right),

the sum ranging over exactly the arms with strictly positive gap.

Hypotheses.

$\nu$ is $1$ -sub-Gaussian: for every arm $i$ , the identity is $P_i$ -integrable, and for every $\lambda\in\mathbb{R}$ the function $x\mapsto e^{\lambda(x-\mu_i)}$ is $P_i$ -integrable with $\int e^{\lambda(x-\mu_i)}\,dP_i\le e^{\lambda^{2}/2}$ .
$\pi$ satisfies the index-policy property above (at every history, reachable or not).
$n\in\mathbb{N}$ is arbitrary.
$(\varepsilon_i)$ is an arbitrary real family subject only to: for each arm $i$ with $\Delta_i>0$ , $0<\varepsilon_i<\Delta_i$ (both inequalities strict).

Edge cases.

For arms with $\Delta_i\le 0$ , $\varepsilon_i$ is completely unconstrained (it may be $0$ ); such arms do not occur in the sum.
In the bound, the schedule is evaluated at the horizon $n$ itself, whereas the policy's index evaluates it at (history length) $+\,1$ . For $n\in\{0,1\}$ , $f(n)=1$ and $\log f(n)=0$ .
For $k=0$ the policy property is unsatisfiable, so the statement holds vacuously there.
$R_n$ carries the stated junk conventions (supremum definition of $\mu^{*}$ ; integral defaulting to $0$ ).

Human review

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

View graph