BanditAlgorithm.bandit_subgaussian_maximal_inequality

Proved

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

concentrationmartingaleprobability

(Maximal concentration) Let $X_0, X_1, \dots$ be independent $\sigma$ -subgaussian ( $\sigma > 0$ ) random variables and $S_t = \sum_{s<t} X_s$ . Then for any $\varepsilon > 0$ and $n \ge 1$ ,

\mathbb{P}\left(\exists\, t \in [1,n] : S_t \ge \varepsilon\right) \le \exp\!\left(-\frac{\varepsilon^2}{2n\sigma^2}\right)

(via Doob's submartingale inequality applied to $\exp(\lambda S_t)$ ).

Preamble

import Mathlib.Probability.Moments.SubGaussian


open MeasureTheory ProbabilityTheory Real NNReal

Formal statement

theorem BanditAlgorithm.bandit_subgaussian_maximal_inequality
    {Ω : Type} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
    {X : ℕ → Ω → ℝ} {σ : ℝ≥0} (hσ : 0 < σ)
    (h_indep : iIndepFun X P)
    (h_subG : ∀ i, HasSubgaussianMGF (X i) (σ ^ 2) P)
    {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) :
    P.real {ω | ∃ t, 0 < t ∧ t ≤ n ∧ ε ≤ ∑ s ∈ Finset.range t, X s ω} ≤
      exp (-ε ^ 2 / (2 * n * (σ : ℝ) ^ 2)) := by
  sorry

Source

L&S Theorem 9.2, p.125

Read-back

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

Setup and notation. Let $(\Omega,\mathcal{F},P)$ carry a probability measure and let $X_0,X_1,\dots:\Omega\to\mathbb{R}$ be a sequence of functions. For $c\ge 0$ , say $Y$ is $c$ -sub-Gaussian in MGF form if for every $\lambda\in\mathbb{R}$ , $e^{\lambda Y}$ is $P$ -integrable and $\int e^{\lambda Y}\,dP\le e^{c\lambda^{2}/2}$ . For a set $S\subseteq\Omega$ , $P(S)$ below denotes the real number obtained from the measure of $S$ (the measure is applied to the set as given — as an outer measure if $S$ is not measurable — and its value in $[0,\infty]$ is converted to a real number, with $\infty\mapsto 0$ ; for a probability measure the value is finite anyway).

Assertion.

P\Bigl(\Bigl\{\omega\ \Big|\ \exists\,t\in\mathbb{N},\ 0<t\le n\ \text{ and }\ \varepsilon\le\sum_{s=0}^{t-1}X_s(\omega)\Bigr\}\Bigr)\ \le\ \exp\!\Bigl(\frac{-\varepsilon^{2}}{2\,n\,\sigma^{2}}\Bigr),

i.e. the probability that some partial sum of the first $t$ variables ( $1\le t\le n$ ) reaches the level $\varepsilon$ is at most the stated Gaussian tail.

Hypotheses.

$P$ is a probability measure.
The entire family $(X_s)_{s\in\mathbb{N}}$ is mutually independent under $P$ .
Each $X_s$ is $\sigma^{2}$ -sub-Gaussian in MGF form.
$\sigma$ is a nonnegative real with $\sigma>0$ ; $n\in\mathbb{N}$ with $n>0$ ; $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$ .

Edge cases.

The event involves the raw partial sums $\sum_{s<t}X_s$ , not averages, and the threshold inequality is non-strict.
The exponent divides by the full range $n$ , not by the individual time $t$ at which the sum crosses.
No centering hypothesis is stated for the $X_s$ beyond what the MGF bound itself expresses, and no separate measurability of the event is hypothesized.

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