Prove2Me

BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound

Proved

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

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

View graph