BanditAlgorithm.bandit_minimax_lower_bound

Proved

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

banditslower-boundsminimax

(Minimax lower bound, GOAL) Let $k > 1$ and $n \ge k-1$ . For any policy $\pi$ there exists a mean vector $\mu \in [0,1]^k$ such that on the unit-variance Gaussian bandit $\nu_\mu$ ,

R_n(\pi, \nu_\mu) \ge \frac{1}{27}\sqrt{(k-1)n}.

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_GaussianBandit


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_minimax_lower_bound {k n : ℕ} (hk : 1 < k) (hn : k - 1 ≤ n)
    (π : BanditPolicy k) :
    ∃ μvec : Fin k → ℝ, (∀ i, μvec i ∈ Set.Icc (0 : ℝ) 1) ∧
      Real.sqrt (((k : ℝ) - 1) * n) / 27 ≤
        banditRegret (gaussianBandit μvec) π n := by
  sorry

Source

L&S Theorem 15.2, p.199 (statement announced as Theorem 13.1, p.180)

View graph