BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

BanditRLwiki case · stochastic-instance-dependent-klucb

Bernoulli KL-UCB instance-dependent asymptotic regret

KL-UCB matches the Lai–Robbins information lower bound arm by arm on Bernoulli bandits.

← Finite stochastic bandits

Audited comparison

stochastic-instance-dependent-klucb Bernoulli KL-UCB instance-dependent asymptotic regretKL-UCB matches the Lai–Robbins information lower bound arm by arm on Bernoulli bandits. Asymptotically matchedPartial local route
Open stable case page →Faithful restatement
KL-UCBLai-RobbinsBernoulli KLinstance dependentasymptotic
Reward model
Stationary Bernoulli arms with a unique best mean
Policy class
Uniformly efficient policies for the lower bound
Regret
Expected pseudo-regret normalized by log T
Target constant
sum over suboptimal arms of Delta_a divided by kl(mu_a, mu_star)

Comparison judgment

Asymptotically matched

The published upper and lower information constants match. Chapter 16's asymptotic and finite-time lower bounds compile; sharp KL-Chernoff concentration for the matching upper constant remains separate.

Known gap. No leading-constant gap in the Bernoulli source model; the local Lean route is a conservative finite-time theorem and does not reach this asymptotic constant.

Local Lean boundary

Partial local route

A measurable generated KL-UCB index, all-time confidence event, pull-count bound, and conservative finite-time expected pseudo-regret theorem compile. Chapter 16 Lemma 16.3 and Gaussian Theorem 16.4 compile, as does the asymptotic Theorem 16.2 lower bound; the sharp KL-UCB upper leading constant remains separate.

Upper bound

KL-UCB asymptotic pull-count upper bound

The KL-UCB Algorithm for Bounded Stochastic Bandits and Beyond

Aurélien Garivier and Olivier Cappé · 2011 · Theorems 1–2 and Corollary 3

Upper bound guarantee. For every suboptimal Bernoulli arm, KL-UCB's expected pull count has the optimal logarithmic leading constant.

Bernoulli specialization of the source's bounded and one-parameter models.

Open primary source

Lower bound

Lai–Robbins asymptotic information lower bound

Asymptotically Efficient Adaptive Allocation Rules

Tze Leung Lai and Herbert Robbins · 1985 · Asymptotic information lower bound

Lower bound guarantee. Every uniformly efficient policy must sample each suboptimal arm at least logarithmically at the information-theoretic rate.

Use the source's regular parametric-family and efficiency assumptions; the displayed Bernoulli form is a specialization.

Open primary source

Not yet proved here

Missing steps

  • Prove sharp KL-Chernoff confidence inversion and the Garivier–Cappé leading constant.
  • Use the compiled Theorem 16.2 lower bound when comparing the remaining sharp upper-bound obligations.

formalization frontier

Can the compiled finite-mean Lemma 16.3 be lifted through d_inf and liminf to the exact KL-UCB leading constant?

The generated conservative KL-UCB route and exact Chapter 16 Lemma 16.3 compile; the d_inf-to-liminf bridge and Theorem 16.2 also compile.

  • d_inf branch analysis
  • liminf terminal
  • sharp KL-UCB upper constant
  • Named formalization leaf: CH16-THM-16-2

Improve this case

Corrections should preserve the comparison signature and cite a primary theorem, theorem number, source edition, and exact gap being closed. Lean contributions should target one named missing leaf without weakening the mathematical contract.

Propose a sourced update