Round-robin empirical maximizer probability bound

Open

BanditAlgorithm.etc_roundRobin_empirical_maximizer_probability_bound

by Zehao Jin · Aug 20, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bandit-algorithmsconcentrationprobability

Let $k>0$ and $m\ge 1$ . Consider a $k$ -armed stochastic bandit whose reward laws are $1$ -subgaussian. A policy explores deterministically in round-robin order for $mk$ rounds, so every arm is sampled exactly $m$ times. If $C$ is any arm attaining the largest empirical mean after exploration, then for every arm $i$ ,

\mathbb P(C=i) \le \exp\!\left(-\frac{m\Delta_i^2}{4}\right),

where $\Delta_i$ is the suboptimality gap of arm $i$ . For an optimal arm the bound is the tautological value $1$ ; for a suboptimal arm it is the two-sample subgaussian comparison bound used in the explore-then-commit analysis.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem etc_roundRobin_empirical_maximizer_probability_bound
    {k : ℕ} (hk : 0 < k)
    {ν : StochasticBandit k}
    (hν : IsSubgaussianBandit 1 ν)
    {m : ℕ} (hm : 1 ≤ m) {π : BanditPolicy k}
    (commit : BanditHistory k (m * k) → Fin k)
    (hmax : ∀ h₀ : BanditHistory k (m * k), ∀ j : Fin k,
      armEmpiricalMean j h₀ ≤ armEmpiricalMean (commit h₀) h₀)
    (hexplore : ∀ (n : ℕ) (h : BanditHistory k n) (hlt : n < m * k),
      (π.select n) h = Measure.dirac ⟨n % k, Nat.mod_lt n hk⟩)
    (i : Fin k) :
    (banditMeasure ν π (m * k)).real {h | commit h = i} ≤
      Real.exp (-(m * (banditGap ν i) ^ 2) / 4) := by sorry

end BanditAlgorithm

Source

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Section 6.1, Theorem 6.1 proof, equation (6.3), printed pp. 92–93 (PDF pp. 101–102), https://tor-lattimore.com/downloads/book/book.pdf

View graph