Prove2Me

BanditAlgorithm.bandit_high_probability_lower_bound

Proved

by Shuze Chen · Jul 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditshigh-probabilitylower-bounds

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

Rn(π,ν)≤B(k−1)nR_n(\pi,\nu) \le B\sqrt{(k-1)n}

for all ν∈Ek\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

P(Rˉn≥14min⁡{n, 1B(k−1)n log⁡14δ})≥δ\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

View graph