Self-normalised deviation bound at a fixed pull count

Proved

BanditAlgorithm.bandit_selfnormalised_fixed_count

by Grace · Jul 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditsconcentrationgaussian

The self-normalised deviation bound at a deterministic pull count: for a unit-variance Gaussian bandit, an arbitrary policy, an arm $a$ , an integer $m\ge1$ and $\beta>0$ ,

\mathbb P\Bigl(T_a(n)=m\ \text{ and }\ \bigl(S_a(n)-T_a(n)\mu_a\bigr)^2\ge 2m\beta\Bigr)\ \le\ 2e^{-\beta}.

Since $\bigl(S_a(n)-T_a(n)\mu_a\bigr)^2/(2T_a(n))=\tfrac12 T_a(n)\bigl(\hat\mu_a(n)-\mu_a\bigr)^2$ , the event is exactly a deviation of the self-normalised statistic appearing in Chernoff's stopping rule, at a fixed count. The proof splits by sign and applies the fixed-tilt Chernoff bound at $\lambda=\pm\sqrt{2\beta/m}$ , the optimal tilt for the count $m$ : on the event it makes $\tfrac{\lambda^2}{2}T_a(n)=\beta$ while $\lambda\bigl(S_a(n)-T_a(n)\mu_a\bigr)\ge2\beta$ , so the martingale exponent already exceeds $\beta$ .

Preamble

import Definitions.Def_TrackAndStop
import Definitions.Def_GaussianBandit

open MeasureTheory ProbabilityTheory NNReal ENNReal
open scoped Classical

Formal statement

theorem BanditAlgorithm.bandit_selfnormalised_fixed_count {k : ℕ} (μvec : Fin k → ℝ)
    (pol : BanditAlgorithm.BanditPolicy k) (a : Fin k) (n : ℕ) {m : ℕ} (hm : 0 < m)
    {β : ℝ} (hβ : 0 < β) :
    BanditAlgorithm.banditTrajMeasure (BanditAlgorithm.gaussianBandit μvec) pol
        {ω : ℕ → Fin k × ℝ | BanditAlgorithm.trajPullCount a n ω = m ∧
          2 * (m : ℝ) * β
            ≤ ((∑ s ∈ (Finset.range n).filter fun s ↦ (ω s).1 = a, (ω s).2)
                - (BanditAlgorithm.trajPullCount a n ω : ℝ) * μvec a) ^ 2}
      ≤ 2 * ENNReal.ofReal (Real.exp (-β)) := by
  sorry

Source

Standard optimisation of the Chernoff tilt at a deterministic pull count; see Garivier & Kaufmann, COLT 2016, Section 4.

View graph