BanditAlgorithm.linear_bandit_asymptotic_lower_bound

Proved

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

asymptoticbanditslinearlower-bounds

(Asymptotic instance-dependent lower bound, L&S Theorem 25.1 + Corollary 25.2) Let $\mathcal{A} = \{a_1,\dots,a_k\} \subset \mathbb{R}^d$ be finite and span $\mathbb{R}^d$ , with unit-variance Gaussian rewards $X_t = \langle A_t,\theta\rangle + \eta_t$ , and let $\pi$ be consistent on the class $\{\nu_{\theta'} : \theta' \in \mathbb{R}^d\}$ (Eq. (25.1): $R_n = o(n^p)$ for all $p>0$ ). Suppose $\theta$ has a unique optimal action, and write $\bar G_n = \mathbb{E}_\theta[\sum_{t=1}^n A_tA_t^\top]$ . Then:

(1) $\liminf_n \lambda_{\min}(\bar G_n)/\log n > 0$ (transcribed as a uniform quadratic-form bound $c\,\log n\,\|v\|^2 \le v^\top \bar G_n v$ eventually);
(2) $\limsup_{n\to\infty} \log(n)\,\|a\|^2_{\bar G_n^{-1}} \le \Delta_a^2/2$ for every $a \in \mathcal{A}$ ;
(3) $\liminf_{n\to\infty} R_n/\log n \ge c(\mathcal{A},\theta)$ , where

c(\mathcal{A},\theta) = \inf_{\alpha \ge 0} \sum_a \alpha(a)\Delta_a \quad\text{subject to}\quad \|a\|^2_{H_\alpha^{-1}} \le \frac{\Delta_a^2}{2} \text{ for all suboptimal } a, \qquad H_\alpha = \sum_a \alpha(a)aa^\top

(allocations restricted to positive-definite $H_\alpha$ ).

Preamble

import Definitions.Def_LinearBanditProtocol
import Definitions.Def_ConsistentBanditPolicy


open Matrix MeasureTheory ProbabilityTheory Filter ENNReal

Formal statement

theorem BanditAlgorithm.linear_bandit_asymptotic_lower_bound {k d : ℕ}
    (arms : Fin k → Fin d → ℝ) (hinj : Function.Injective arms)
    (hspan : Submodule.span ℝ (Set.range arms) = ⊤)
    (π : BanditPolicy k)
    (hcons : IsConsistentPolicy
      {ν : StochasticBandit k | ∃ θ' : Fin d → ℝ, ν = gaussianLinearBandit arms θ'} π)
    (θ : Fin d → ℝ) (jstar : Fin k)
    (hopt : ∀ j : Fin k, j ≠ jstar → arms j ⬝ᵥ θ < arms jstar ⬝ᵥ θ) :
    (∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, ∀ v : Fin d → ℝ,
        c * Real.log n * (v ⬝ᵥ v) ≤
          v ⬝ᵥ linearBanditExpectedDesign arms (gaussianLinearBandit arms θ) π n *ᵥ v) ∧
    (∀ j : Fin k,
      atTop.limsup (fun n : ℕ ↦ ENNReal.ofReal (Real.log n *
          (arms j ⬝ᵥ
            (linearBanditExpectedDesign arms (gaussianLinearBandit arms θ) π n)⁻¹ *ᵥ
            arms j))) ≤
        ENNReal.ofReal (linearArmGap arms θ j ^ 2 / 2)) ∧
    ENNReal.ofReal (linearBanditAllocationValue arms θ) ≤
      atTop.liminf (fun n : ℕ ↦
        ENNReal.ofReal (banditRegret (gaussianLinearBandit arms θ) π n / Real.log n)) := by
  sorry

Source

L&S Theorem 25.1 + Corollary 25.2, pp.296-297

Read-back

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

Fix $k$ arm vectors $a^{(1)},\dots,a^{(k)}\in\mathbb R^d$ . For $\theta'\in\mathbb R^d$ , let $\nu_{\theta'}$ be the $k$ -armed stochastic bandit whose arm $j$ has reward distribution $\mathcal N\big(\langle a^{(j)},\theta'\rangle,1\big)$ ; let $\mathcal G=\{\nu_{\theta'}:\theta'\in\mathbb R^d\}$ . A $k$ -armed policy $\pi$ is a family of per-round probability kernels from finite histories of (arm index, reward) pairs to arm indices; the interaction law $\mathbb P^{\nu,\pi}_n$ on length- $n$ histories is built recursively (arm drawn from the kernel applied to the past, reward drawn from that arm's distribution). Write $\mu_i(\nu)$ for the mean of arm $i$ 's distribution, $R_n(\nu)=n\,\sup_i\mu_i(\nu)-\int\sum_{t<n}x_t\,d\mathbb P^{\nu,\pi}_n$ for the expected regret (sum of realized rewards), $T_j(n)$ for the number of pulls of arm $j$ in $n$ rounds, $\bar G_n=\sum_{j}\mathbb E_{\nu_\theta,\pi}\big[T_j(n)\big]\,a^{(j)}(a^{(j)})^{\top}$ for the expected design matrix under $\nu_\theta$ , $\Delta_j=\sup_{j'}\langle a^{(j')},\theta\rangle-\langle a^{(j)},\theta\rangle$ for the gaps, and

c^{\ast}(\theta)=\inf\Big\{\sum_j\alpha_j\Delta_j\ :\ \alpha_j\ge0,\ H(\alpha)=\textstyle\sum_j\alpha_j a^{(j)}(a^{(j)})^{\top}\ \text{positive definite},\ \forall j\,\big(\Delta_j>0\Rightarrow (a^{(j)})^{\top}H(\alpha)^{-1}a^{(j)}\le\Delta_j^2/2\big)\Big\}.

Finally write $[x]_+$ for the real number $x$ truncated at $0$ and regarded as an element of $[0,\infty]$ , and $\ln$ for the natural logarithm.

The theorem asserts the conjunction of three claims:

\text{(i)}\quad\exists\,c>0\ \text{such that for all sufficiently large }n,\ \forall v\in\mathbb R^d:\quad c\,(\ln n)\,\langle v,v\rangle\ \le\ v^{\top}\bar G_n\,v;

\text{(ii)}\quad\forall j\in\{1,\dots,k\}:\quad \limsup_{n\to\infty}\ \Big[\ln n\cdot\big(a^{(j)}\big)^{\top}\bar G_n^{-1}\,a^{(j)}\Big]_+\ \le\ \Big[\Delta_j^{\,2}/2\Big]_+;

\text{(iii)}\quad \big[c^{\ast}(\theta)\big]_+\ \le\ \liminf_{n\to\infty}\ \Big[\,R_n(\nu_\theta)\,/\,\ln n\,\Big]_+,

where the limit superior/inferior in (ii) and (iii) are taken in $[0,\infty]$ .

Hypotheses:

The map $j\mapsto a^{(j)}$ is injective, and the arm vectors span all of $\mathbb R^d$ .
$\pi$ is consistent on $\mathcal G$ : for every $\nu\in\mathcal G$ and every real $p>0$ , $R_n(\nu)/n^{p}\to 0$ as $n\to\infty$ .
$\theta\in\mathbb R^d$ and $j^{\ast}$ is an arm index with $\langle a^{(j)},\theta\rangle<\langle a^{(j^{\ast})},\theta\rangle$ for every $j\ne j^{\ast}$ (unique strict optimality).

Edge cases and conventions:

The truncation $[\cdot]_+$ discards all sign information: any negative quantity becomes $0$ before the $\limsup$ / $\liminf$ is taken.
$\bar G_n^{-1}$ is the junk-convention inverse, equal to the zero matrix whenever $\bar G_n$ is singular (making the quadratic form in (ii) equal to $0$ at such $n$ ).
Claim (ii) includes $j=j^{\ast}$ ; there $\Delta_{j^{\ast}}=0$ by the optimality hypothesis, so the claim forces the corresponding limit superior to equal $0$ .
For $n\in\{0,1\}$ , $\ln n=0$ (with $\ln 0=0$ by convention) and the real division in (iii) by $\ln n=0$ yields $0$ ; these finitely many terms do not affect the asymptotic statements.
If the allocation program in $c^{\ast}(\theta)$ is infeasible, its value is the real-infimum junk value $0$ and claim (iii) is trivially true.
In (i) the constant $c$ is chosen first, then the bound is required for all large enough $n$ and all vectors $v$ simultaneously.

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