BanditAlgorithm.bandit_high_probability_lower_bound

Proved

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

banditshigh-probabilitylower-bounds

(High-probability lower bound, stochastic) Suppose a policy $\pi$ satisfies

R_n(\pi,\nu) \le B\sqrt{(k-1)n}

for all $\nu \in \mathcal{E}^k$ (Gaussian bandits with suboptimality gaps at most 1). Then for every $\delta$ there exists a bandit $\nu$ in the class with

\mathbb{P}\left(\bar R_n \ge \frac{1}{4}\min\Big\{n,\ \frac{1}{B}\sqrt{(k-1)n}\,\log\frac{1}{4\delta}\Big\}\right) \ge \delta

— expected-regret optimality forces heavy tails on the random regret.

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_GaussianBandit


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_high_probability_lower_bound {k n : ℕ} (hk : 2 ≤ k) (hn : 1 ≤ n)
    {B : ℝ} (hB : 0 < B) (π : BanditPolicy k)
    (hbound : ∀ μvec : Fin k → ℝ, (∀ i, μvec i ∈ Set.Icc (0 : ℝ) 1) →
      banditRegret (gaussianBandit μvec) π n ≤ B * Real.sqrt (((k : ℝ) - 1) * n))
    {δ : ℝ} (hδ : δ ∈ Set.Ioo (0 : ℝ) 1) :
    ∃ μvec : Fin k → ℝ, (∀ i, μvec i ∈ Set.Icc (0 : ℝ) 1) ∧
      δ ≤ (banditMeasure (gaussianBandit μvec) π n).real
        {h | (1 / 4 : ℝ) * min (n : ℝ)
              (Real.sqrt (((k : ℝ) - 1) * n) * Real.log (1 / (4 * δ)) / B) ≤
            ∑ i, (armPullCount i h : ℝ) * banditGap (gaussianBandit μvec) i} := by
  sorry

Source

L&S Theorem 17.1, p.216

Read-back

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

Setup and notation. For a real vector $\mu=(\mu_i)_{i<k}$ , let $\nu_\mu$ be the Gaussian bandit whose arm- $i$ distribution is $\mathcal{N}(\mu_i,1)$ (variance $1$ ). Write $m_i$ for the Bochner-integral mean of arm $i$ 's distribution, $m^{*}=\sup_i m_i$ , and $\Delta_i(\mu)=m^{*}-m_i$ for the gaps of $\nu_\mu$ . For a policy $\pi$ , $\mathbb{P}^{n}_{\mu}$ is the canonical probability measure on length- $n$ histories of $\nu_\mu$ under $\pi$ (empty-history point mass, then repeatedly: arm from the policy kernel given the history, reward from that arm, pair appended); $T_i(h)$ is the number of rounds of the history $h$ playing arm $i$ ; $R_n(\mu)=n\,m^{*}-\int\bigl(\sum_{t<n}X_t\bigr)d\mathbb{P}^{n}_{\mu}$ is the expected regret (defaulting-integral convention). $\mathbb{P}^{n}_{\mu}(\cdot)$ applied to a set below denotes the real number obtained from the measure of that set.

Assertion. There exists a mean vector $\mu\in[0,1]^{k}$ such that

\delta\ \le\ \mathbb{P}^{n}_{\mu}\left(\left\{h\ \middle|\ \frac{1}{4}\,\min\!\Bigl(n,\ \frac{\sqrt{(k-1)\,n}\;\log\frac{1}{4\delta}}{B}\Bigr)\ \le\ \sum_{i=0}^{k-1}T_i(h)\,\Delta_i(\mu)\right\}\right),

i.e. under the witness instance, with probability at least $\delta$ the realized history's pull-count-weighted sum of gaps reaches the displayed threshold.

Hypotheses.

$2\le k$ and $1\le n$ .
$B>0$ is real.
Uniform regret bound on the cube: for every vector $\mu'\in[0,1]^{k}$ (componentwise), $R_n(\mu')\le B\,\sqrt{(k-1)\,n}$ , at this same horizon $n$ .
$\delta\in(0,1)$ (open interval, both inequalities strict).

Edge cases.

If $\delta\ge\tfrac14$ then $\log\frac{1}{4\delta}\le 0$ and the threshold inside the event is nonpositive.
The uniform regret hypothesis constrains $\pi$ only on mean vectors inside $[0,1]^{k}$ ; the witness is also only guaranteed inside the cube.
Both the threshold comparison in the event and the probability bound $\delta\le\cdot$ are non-strict; the sum in the event runs over all $k$ arms.
In the display, $k$ , $n$ and the pull counts are cast to reals ( $k-1$ is real subtraction); the measure of the event set is taken as-is and converted to a real number.
$R_n$ and the gaps carry the stated conventions (supremum optimal mean; Bochner integrals defaulting to $0$ ).

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