Prove2Me

BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound

Proved

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

banditslinearlower-boundsminimax

(Hypercube lower bound, L&S Theorem 24.1) Let A=[−1,1]d\mathcal{A} = [-1,1]^d and Θ={−n−1/2,n−1/2}d\Theta = \{-n^{-1/2}, n^{-1/2}\}^d, with unit-variance Gaussian noise Xt=⟨At,θ⟩+ηtX_t = \langle A_t,\theta\rangle + \eta_t, ηt∼N(0,1)\eta_t \sim \mathcal{N}(0,1). Then, for any policy supported in A\mathcal{A}, there exists θ∈Θ\theta \in \Theta such that

Rn(A,θ)≥e−28 dn.R_n(\mathcal{A},\theta) \ge \frac{e^{-2}}{8}\, d\sqrt{n}.

(The book states no further conditions; d≥1d \ge 1, n≥1n \ge 1 are the chapter's standing assumptions.)

Preamble
import Definitions.Def_LinearBanditProtocol


open Matrix MeasureTheory
Formal statement
theorem BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound {d n : ℕ}
    (hd : 0 < d) (hn : 0 < n) (π : LinearBanditPolicy d)
    (hsupp : IsSupportedLinearPolicy {a : Fin d → ℝ | ∀ i, |a i| ≤ 1} π) :
    ∃ θ : Fin d → ℝ,
      (∀ i, θ i = Real.sqrt (1 / n) ∨ θ i = -Real.sqrt (1 / n)) ∧
      Real.exp (-2) / 8 * (d * Real.sqrt n) ≤
        linearBanditExpectedRegret {a : Fin d → ℝ | ∀ i, |a i| ≤ 1} θ π n := by
  sorry
Source
L&S Theorem 24.1, p.289
Read-back

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

Consider the dd-dimensional linear stochastic bandit protocol: a policy π\pi assigns to each round nn a probability kernel πn\pi_n from length-nn histories of action–reward pairs ((a0,x0),…,(an−1,xn−1))∈(Rd×R)n\big((a_0,x_0),\dots,(a_{n-1},x_{n-1})\big)\in(\mathbb R^d\times\mathbb R)^n to actions in Rd\mathbb R^d. For a parameter θ∈Rd\theta\in\mathbb R^d, the law Pnθ\mathbb P^{\theta}_n of the length-nn history is built recursively: at each round an action AA is drawn from the policy kernel applied to the past, and the recorded reward is ⟨A,θ⟩+Z\langle A,\theta\rangle+Z with Z∼N(0,1)Z\sim\mathcal N(0,1) independent standard Gaussian. The expected regret over the action set A={a∈Rd: ∣ai∣≤1 for all i}\mathcal A=\{a\in\mathbb R^d:\ |a_i|\le 1\ \text{for all }i\} (the closed hypercube [−1,1]d[-1,1]^d) is

Rn(θ)  =  n⋅sup⁡{⟨a,θ⟩:a∈A}  −  ∫∑t=0n−1⟨at,θ⟩ dPnθ.R_n(\theta)\;=\;n\cdot\sup\{\langle a,\theta\rangle : a\in\mathcal A\}\;-\;\int\sum_{t=0}^{n-1}\langle a_t,\theta\rangle\ d\mathbb P^{\theta}_n .

The theorem asserts:

∃ θ∈Rd with θi∈{1/n, −1/n} for every i,e−28⋅d n ≤ Rn(θ).\exists\,\theta\in\mathbb R^d\ \text{with}\ \theta_i\in\big\{\sqrt{1/n},\,-\sqrt{1/n}\big\}\ \text{for every }i,\qquad \frac{e^{-2}}{8}\cdot d\,\sqrt n\ \le\ R_n(\theta).

Hypotheses:

  • d>0d>0 and n>0n>0 (natural numbers).
  • π\pi is an arbitrary dd-dimensional linear bandit policy.
  • π\pi is supported on the hypercube: for every round n′n' and every history hh, πn′(h)\pi_{n'}(h) assigns probability 00 to the complement of A\mathcal A.

Edge cases and conventions:

  • The claim is existential: a single hard parameter θ\theta suffices, and it is only pinned to have every coordinate equal to +1/n+\sqrt{1/n} or −1/n-\sqrt{1/n}; which sign pattern is not specified.
  • The regret's expectation term is a Bochner integral and silently equals 00 if the sum of mean rewards fails to be integrable; the supremum term is the real supremum over the hypercube.
  • The reward noise is exactly unit-variance Gaussian; the bound constant is e−2/8≈0.0169e^{-2}/8\approx 0.0169.
Human review

  • Endorsed by Community (Bot) · Jul 29, 2026

  • Endorsed by Shuze Chen · Jul 29, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph