Pairwise empirical-mean tail bound under round-robin sampling

Proved

BanditAlgorithm.roundRobin_empirical_mean_pairwise_tail

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

bandit-algorithmsconcentrationprobabilitysubgaussian

Let $k>0$ and $m\ge 1$ . In a $1$ -subgaussian stochastic bandit, suppose the first $mk$ actions sample the arms deterministically in round-robin order, giving exactly $m$ observations from each arm. Fix an arm $i$ and an optimal arm $j$ . Then

\mathbb P(\widehat\mu_j \le \widehat\mu_i) \le \exp\!\left(-\frac{m\Delta_i^2}{4}\right),

where $\Delta_i=\mu_j-\mu_i$ . This is the fixed-pair, two-sample subgaussian comparison inequality underlying the explore-then-commit error bound.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem roundRobin_empirical_mean_pairwise_tail
    {k : ℕ} (hk : 0 < k)
    {ν : StochasticBandit k}
    (hν : IsSubgaussianBandit 1 ν)
    {m : ℕ} (hm : 1 ≤ m) {π : BanditPolicy k}
    (hexplore : ∀ (n : ℕ) (h : BanditHistory k n) (hlt : n < m * k),
      (π.select n) h = Measure.dirac ⟨n % k, Nat.mod_lt n hk⟩)
    (i j : Fin k) (hj : banditArmMean ν j = banditOptimalMean ν) :
    (banditMeasure ν π (m * k)).real
        {h | armEmpiricalMean j h ≤ armEmpiricalMean i h} ≤
      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, proof of Theorem 6.1, equation (6.3), printed pp. 92–93 (PDF pp. 101–102), https://tor-lattimore.com/downloads/book/book.pdf

View graph