Pairwise centered MGF bound under round-robin sampling

Open

BanditAlgorithm.roundRobin_pairwise_centered_mgf_bound

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

bandit-algorithmsconcentrationmgfprobabilitysubgaussian

Let a $1$ -subgaussian stochastic bandit be sampled in deterministic round-robin order for $mk$ rounds, producing $m$ samples from every arm. For arms $i,j$ , define the scaled difference of centered empirical means by

X=m\big[(\widehat\mu_i-\mu_i)-(\widehat\mu_j-\mu_j)\big].

Then $e^{tX}$ is integrable for every $t\in\mathbb R$ , and

\mathbb E[e^{tX}]\le \exp(mt^2).

Thus $X$ is subgaussian with variance proxy $2m$ . The statement packages the exact exponential-moment estimate needed for the two-arm Chernoff comparison in explore-then-commit.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem roundRobin_pairwise_centered_mgf_bound
    {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) (t : ℝ) :
    let X : BanditHistory k (m * k) → ℝ := fun h ↦
      (m : ℝ) * ((armEmpiricalMean i h - banditArmMean ν i) -
        (armEmpiricalMean j h - banditArmMean ν j))
    Integrable (fun h ↦ Real.exp (t * X h)) (banditMeasure ν π (m * k)) ∧
      ∫ h, Real.exp (t * X h) ∂banditMeasure ν π (m * k) ≤
        Real.exp ((m : ℝ) * t ^ 2) := 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 leading to equation (6.3), printed pp. 92–93 (PDF pp. 101–102), https://tor-lattimore.com/downloads/book/book.pdf

View graph