BanditAlgorithm.bandit_asymptotically_optimal_ucb_limsup

Proved

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

asymptoticbanditsregretucb

(Asymptotic optimality) For any 1-subgaussian $k$ -armed bandit and any instance of Algorithm 6,

\limsup_{n\to\infty} \frac{R_n}{\log n} \le \sum_{i:\Delta_i>0} \frac{2}{\Delta_i}

— matching the Lai–Robbins lower bound (Mission VII) for unit-variance Gaussian rewards. Stated in $[0,\infty]$ via ENNReal.ofReal on both sides (mirroring the Mission VII liminf convention) so the limsup needs no boundedness side conditions.

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_asymptoticUcbPolicy


open MeasureTheory ProbabilityTheory Filter

Formal statement

theorem BanditAlgorithm.bandit_asymptotically_optimal_ucb_limsup {k : ℕ}
    {ν : StochasticBandit k} (hν : IsSubgaussianBandit 1 ν)
    {π : BanditPolicy k} (hπ : IsAsymptoticUCBPolicy π) :
    atTop.limsup
        (fun n : ℕ ↦ ENNReal.ofReal (banditRegret ν π n / Real.log n)) ≤
      ∑ i ∈ Finset.univ.filter (fun i ↦ 0 < banditGap ν i),
        ENNReal.ofReal (2 / banditGap ν i) := by
  sorry

Source

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

View graph