BanditAlgorithm.bandit_minimax_lower_bound

Proved

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

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)

Read-back

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

Setup and notation. For a real vector $(\mu_i)_{i<k}$ , let $\nu_\mu$ be the Gaussian bandit whose arm- $i$ distribution is $\mathcal{N}(\mu_i,1)$ (variance $1$ ). For a policy $\pi$ (family of Markov kernels from histories to arm distributions), $\mathbb{P}^{n}$ is the canonical measure on length- $n$ histories (empty history point mass, then repeatedly: arm from the policy kernel, reward from that arm's distribution, pair appended), and the expected regret is

R_n(\nu_\mu,\pi)=n\,\mu^{*}-\int\Bigl(\sum_{t<n}X_t\Bigr)d\mathbb{P}^{n},

where $\mu^{*}$ is the supremum over arms of the (Bochner-integral) mean of the arm's distribution, and the integral defaults to $0$ if the total reward is not integrable.

Assertion. There exists a mean vector $(\mu_i)_{i<k}$ with every $\mu_i\in[0,1]$ such that

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

Hypotheses.

$1<k$ (that is, $k\ge 2$ ).
$k-1\le n$ , stated with natural-number subtraction (given $k\ge2$ this coincides with ordinary $k-1\le n$ ).
$\pi$ is an arbitrary policy; $n$ is the same horizon in the hypothesis and the regret.

Edge cases.

In the displayed bound, $k$ , $n$ are cast to reals and $k-1$ is real subtraction.
Only the existence of one mean vector inside the cube $[0,1]^{k}$ is asserted; nothing is claimed about vectors outside the cube, and the witness is not further specified.
The inequality is non-strict, with the explicit constant $\tfrac{1}{27}$ .
$R_n$ carries the stated junk conventions (supremum optimal mean; defaulting integral).

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