BanditAlgorithm.bandit_ucb_index_count_bound

Proved

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

banditsconcentration

(Core counting lemma) Let $X_0, X_1, \dots$ be independent 1-subgaussian random variables (Mathlib's HasSubgaussianMGF with variance proxy 1) on a probability space, and let $\hat\mu_t = \frac{1}{t}\sum_{s<t} X_s$ be the sample mean of the first $t$ of them. For $\varepsilon > 0$ , $a > 0$ and the real-valued sum of indicators

\kappa = \sum_{t=1}^n \mathbb{1}\left\{\hat\mu_t + \sqrt{\frac{2a}{t}} \ge \varepsilon\right\},

the expectation satisfies

\mathbb{E}[\kappa] \le 1 + \frac{2}{\varepsilon^2}\left(a + \sqrt{\pi a} + 1\right).

Preamble

import Mathlib.Probability.Moments.SubGaussian
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic


open MeasureTheory ProbabilityTheory Real

Formal statement

theorem BanditAlgorithm.bandit_ucb_index_count_bound
    {Ω : Type} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
    {X : ℕ → Ω → ℝ}
    (h_indep : iIndepFun X P)
    (h_subG : ∀ i, HasSubgaussianMGF (X i) 1 P)
    {n : ℕ} {ε a : ℝ} (hε : 0 < ε) (ha : 0 < a) :
    ∫ ω, (∑ t ∈ Finset.Icc 1 n,
        if ε ≤ (∑ s ∈ Finset.range t, X s ω) / t + Real.sqrt (2 * a / t)
          then (1 : ℝ) else 0) ∂P ≤
      1 + 2 / ε ^ 2 * (a + Real.sqrt (Real.pi * a) + 1) := by
  sorry

Source

L&S Lemma 8.2, p.118

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setup and notation. Let $(\Omega,\mathcal{F},P)$ be a measurable space equipped with a probability measure and let $X_0,X_1,X_2,\dots:\Omega\to\mathbb{R}$ be a sequence of functions. Say a function $Y$ is $c$ -sub-Gaussian in MGF form under $P$ if for every $\lambda\in\mathbb{R}$ the function $e^{\lambda Y}$ is $P$ -integrable and $\int e^{\lambda Y}\,dP\le e^{c\lambda^{2}/2}$ .

Assertion.

\int_{\Omega}\ \sum_{t=1}^{n}\mathbf{1}\!\left[\ \varepsilon\ \le\ \frac{1}{t}\sum_{s=0}^{t-1}X_s(\omega)\ +\ \sqrt{\frac{2a}{t}}\ \right]dP(\omega)\ \le\ 1+\frac{2}{\varepsilon^{2}}\Bigl(a+\sqrt{\pi a}+1\Bigr),

i.e. the expected number of indices $t\in\{1,\dots,n\}$ at which the average of the first $t$ variables $X_0,\dots,X_{t-1}$ plus the bonus $\sqrt{2a/t}$ reaches (non-strictly) the level $\varepsilon$ is at most the right-hand side. The indicator takes the value $1$ when the bracketed inequality holds and $0$ otherwise.

Hypotheses.

$P$ is a probability measure on $\Omega$ .
The entire infinite family $(X_s)_{s\in\mathbb{N}}$ is mutually independent under $P$ .
Every $X_s$ is $1$ -sub-Gaussian in MGF form.
$n\in\mathbb{N}$ is arbitrary (including $0$ ); $\varepsilon>0$ and $a>0$ are real.

Edge cases.

For $n=0$ the sum is empty, the left side is $0$ , and the claim reduces to nonnegativity of the right side.
Within the summation range $1\le t\le n$ no division by zero occurs.
Nothing is assumed about centering or identical distribution of the $X_s$ ; only independence and the individual MGF bounds appear (integrability of each $e^{\lambda X_s}$ is part of the sub-Gaussian property, and no other measurability hypothesis is stated).
Both the inequality inside the indicator and the final bound are non-strict.

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