BanditAlgorithm.bandit_instance_dependent_lower_bound

Disproved

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

asymptoticbanditslower-bounds

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

(Instance-dependent asymptotic lower bound, Lai–Robbins style) Let $\mathcal{E} = \mathcal{M}_1 \times \cdots \times \mathcal{M}_k$ be an unstructured class and $\pi$ a consistent policy over $\mathcal{E}$ . Then for all $\nu = (P_i)_i \in \mathcal{E}$ :

\liminf_{n\to\infty} \frac{R_n(\pi,\nu)}{\log n} \ge c^*(\nu,\mathcal{E}) = \sum_{i:\Delta_i>0} \frac{\Delta_i}{d_{\inf}(P_i, \mu^*, \mathcal{M}_i)}.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.bandit_instance_dependent_lower_bound {k : ℕ}
    (𝓜 : Fin k → Set (Measure ℝ)) (π : BanditPolicy k)
    (hcons : IsConsistentPolicy {ν : StochasticBandit k | ∀ i, ν.P i ∈ 𝓜 i} π)
    (ν : StochasticBandit k) (hν : ∀ i, ν.P i ∈ 𝓜 i) :
    ∑ i ∈ Finset.univ.filter (fun i ↦ 0 < banditGap ν i),
        ENNReal.ofReal (banditGap ν i) /
          banditDInf (𝓜 i) (ν.P i) (banditOptimalMean ν) ≤
      atTop.liminf
        (fun n : ℕ ↦ ENNReal.ofReal (banditRegret ν π n / Real.log n)) := by
  sorry

Consistency quantifies probability bandit environments, while the KL alternative infimum admits arbitrary measures including measures of mass three.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Restrict every arm model class to probability measures with finite first moment, and use the same admissible environment class in consistency and in the KL alternative infimum.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.

Preamble

import Definitions.Def_ConsistentBanditPolicy


open MeasureTheory ProbabilityTheory Filter

Formal statement

theorem BanditAlgorithm.bandit_instance_dependent_lower_bound {k : ℕ}
    (𝓜 : Fin k → Set (Measure ℝ)) (π : BanditPolicy k)
    (hcons : IsConsistentPolicy {ν : StochasticBandit k | ∀ i, ν.P i ∈ 𝓜 i} π)
    (ν : StochasticBandit k) (hν : ∀ i, ν.P i ∈ 𝓜 i) :
    ∑ i ∈ Finset.univ.filter (fun i ↦ 0 < banditGap ν i),
        ENNReal.ofReal (banditGap ν i) /
          banditDInf (𝓜 i) (ν.P i) (banditOptimalMean ν) ≤
      atTop.liminf
        (fun n : ℕ ↦ ENNReal.ofReal (banditRegret ν π n / Real.log n)) := by
  sorry

Source

L&S Theorem 16.2, Eq. (16.2), p.207

Read-back

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

Setup and notation. Fix per-arm classes $\mathcal{M}_0,\dots,\mathcal{M}_{k-1}$ of measures on $\mathbb{R}$ and let $\mathcal{E}=\{\nu \mid \forall i,\ \nu_i\in\mathcal{M}_i\}$ be the class of $k$ -armed bandits whose arm- $i$ distribution lies in $\mathcal{M}_i$ for every $i$ simultaneously. For a bandit $\nu=(P_i)$ write $\mu_i=\int x\,dP_i$ (Bochner mean, $0$ if not integrable), $\mu^{*}=\sup_i\mu_i$ , $\Delta_i=\mu^{*}-\mu_i$ , and $R_n$ for the expected regret of $\nu$ under the policy $\pi$ at horizon $n$ ( $R_n=n\mu^{*}$ minus the expected total reward under the canonical history measure, with the defaulting-integral convention). $D(\rho\Vert Q)$ is the $[0,\infty]$ -valued Kullback–Leibler divergence ( $+\infty$ without absolute continuity plus integrable log-likelihood ratio), and

D_{\inf}(\mathcal{M},\rho,\mu^{*})=\inf\bigl\{D(\rho\Vert Q)\ \bigm|\ Q\in\mathcal{M},\ \mu^{*}<\textstyle\int x\,dQ\bigr\}\in[0,\infty]

(infimum $=\infty$ over an empty collection; means of competitors are Bochner integrals with the $0$ default; strict threshold). Consistency of $\pi$ on $\mathcal{E}$ means: for every $\nu'\in\mathcal{E}$ and every real $p>0$ , $R_n(\nu',\pi)/n^{p}\to 0$ as $n\to\infty$ (real limit, $n^p$ the real power). Write $(x)^{+}=\max(x,0)$ viewed in $[0,\infty]$ .

Assertion.

\sum_{i:\,\Delta_i>0}\ \frac{(\Delta_i)^{+}}{D_{\inf}\bigl(\mathcal{M}_i,\ P_i,\ \mu^{*}\bigr)}\ \le\ \liminf_{n\to\infty}\ \Bigl(\frac{R_n}{\log n}\Bigr)^{\!+}\qquad\text{in }[0,\infty],

with extended division: $x/\infty=0$ , $x/0=\infty$ for $x\neq0$ , $0/0=0$ ; the sum ranges over the arms with strictly positive gap, where $(\Delta_i)^{+}=\Delta_i$ .

Hypotheses.

$\pi$ is consistent on the entire class $\mathcal{E}$ (every bandit whose arms lie componentwise in the classes).
$\nu$ is a $k$ -armed bandit with $P_i\in\mathcal{M}_i$ for every $i$ .

Edge cases.

A term with $D_{\inf}=\infty$ (e.g. no competitor in $\mathcal{M}_i$ with mean strictly above $\mu^{*}$ ) contributes $0$ .
A term with $D_{\inf}=0$ and $\Delta_i>0$ equals $\infty$ , in which case the claim forces the liminf itself to be $\infty$ .
In the liminf sequence, the terms at $n\in\{0,1\}$ are $0$ (since $\log 0=\log 1=0$ and real division by zero gives $0$ ), and any negative value of $R_n/\log n$ is truncated to $0$ .
Only a non-strict lower bound on the limit inferior is asserted; no matching upper bound and nothing about a limit.

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