BanditAlgorithm.bandit_moss_minimax_regret_bound

Proved

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

banditsminimaxregret

(MOSS minimax optimality) Consider any 1-subgaussian $k$ -armed bandit and any policy that is an instance of MOSS at horizon $n$ (Algorithm 7: play each arm once, then

A_t = \arg\max_i\ \hat\mu_i(t-1) + \sqrt{\frac{4}{T_i(t-1)}\log^+\!\left(\frac{n}{k\,T_i(t-1)}\right)}

with $\log^+(x) = \log\max\{1, x\}$ ). If $k \le n$ (implicit in the book: the algorithm plays each arm once before using the index) then

R_n \le 39\sqrt{kn} + \sum_{i=1}^k \Delta_i.

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_mossPolicy


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_moss_minimax_regret_bound {k : ℕ}
    {ν : StochasticBandit k} (hν : IsSubgaussianBandit 1 ν)
    {n : ℕ} {π : BanditPolicy k} (hπ : IsMOSSPolicy n π) (hkn : k ≤ n) :
    banditRegret ν π n ≤
      39 * Real.sqrt ((k : ℝ) * n) + ∑ i, banditGap ν i := by
  sorry

Source

L&S Theorem 9.1, p.124

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}$ , with means $\mu_i=\int x\,dP_i$ (Bochner integral, $0$ if not integrable), $\mu^{*}=\sup_i\mu_i$ ( $=0$ for $k=0$ ), gaps $\Delta_i=\mu^{*}-\mu_i$ . $\mathbb{P}^{n}_{\nu,\pi}$ is the canonical measure on length- $n$ histories generated by a policy $\pi$ (arm from the policy kernel given the history, reward from that arm's distribution, appended step by step from the empty history), and the expected regret is $R_n=n\mu^{*}-\int\bigl(\sum_{t<n}X_t\bigr)d\mathbb{P}^{n}_{\nu,\pi}$ (integral $=0$ by convention if the total reward is not integrable). With $T_i(h)$ , $\hat\mu_i(h)$ the pull count and empirical mean at a history $h$ (both $0$ for unpulled arms via $x/0=0$ ), $\log^{+}(x)=\log(\max(1,x))$ , and horizon parameter $m$ , the index is $\gamma^{m}_i(h)=\hat\mu_i(h)+\sqrt{\tfrac{4}{T_i(h)}\log^{+}\!\bigl(\tfrac{m}{k\,T_i(h)}\bigr)}$ (conventions: $T_i(h)=0$ makes both fractions $0$ and the index $0$ ). The policy property with parameter $m$ : at every history $h$ of every length there is an arm $a$ selected with probability one (the kernel equals $\delta_a$ ), which is unpulled whenever some arm is unpulled, and which non-strictly maximizes $\gamma^{m}$ over all arms whenever every arm has been pulled.

Assertion.

R_n\ \le\ 39\,\sqrt{k\,n}\ +\ \sum_{i=0}^{k-1}\Delta_i,

where the last sum runs over all $k$ arms.

Hypotheses.

$\nu$ is $1$ -sub-Gaussian: each arm's identity is integrable, and each centered variable $x\mapsto x-\mu_i$ satisfies the MGF bound $\int e^{\lambda(x-\mu_i)}dP_i\le e^{\lambda^{2}/2}$ (with integrability) for all real $\lambda$ .
$\pi$ satisfies the index-policy property with horizon parameter equal to this same $n$ .
$k\le n$ .

Edge cases.

The additive term sums the gaps of all arms, including arms of maximal mean, not only suboptimal arms.
For $k=0$ the policy property is unsatisfiable, so the statement holds vacuously.
$R_n$ carries the stated conventions (supremum $\mu^{*}$ ; total-reward integral defaulting to $0$ ).
The bound is non-strict, with explicit constant $39$ .

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