BanditRLwiki setting
Finite stochastic bandits
Expected, asymptotic, and instance-dependent regret under stationary independent arm rewards.
← All settings
Comparison signature
- Problem class. Finite-armed stationary stochastic bandits
- Feedback. Bandit feedback from the selected arm
- Objective. Expected pseudo-regret unless a case says otherwise
- Parameters. A arms, T rounds, gaps Delta, confidence delta when present
Matching rule. A rate is called matched only when the upper and lower theorem contracts agree on the fields above; every remaining mismatch is named in the case.
2 cases
stochastic-finite-arm-minimax
Finite-arm stochastic minimax expected regretMOSS-type algorithms and Gaussian/Bernoulli hard families identify the square-root A times T minimax scale.
Minimax matchedPartial local route
MOSSminimaxexpected pseudo-regretbounded rewardsGaussian lower bound
- Reward model
- Independent stationary rewards; the literature upper uses rewards in [0,1]
- Horizon
- Any finite T; the cited MOSS-anytime result is horizon-free
- Regret
- Expected pseudo-regret
- Target scale
- Theta(sqrt(A T))
Comparison judgment
Minimax matched
The literature establishes the square-root minimax order. Local Lean now supplies the unit-Gaussian lower bound and fixed-horizon Algorithm 7 on unit-subgaussian laws with gaps in [0,1]. The cited anytime theorem remains a distinct formalization target.
Known gap. Universal constants and the exact hard-family reward class differ across the displayed source theorems.
Local Lean boundary
Partial local route
BanditRLlib compiles a unit-variance Gaussian lower bound with constant 1/54 and fixed-horizon MOSS on unit-subgaussian laws with gaps in [0,1]. The cited anytime MOSS theorem is not compiled.
Upper bound
Anytime MOSS regret
Anytime optimal algorithms in stochastic multi-armed bandits
Rémy Degenne and Vianney Perchet · 2016 · Theorem 3 with Lemma 3
Upper bound guarantee. Formula renderer unavailable; readable fallback: The anytime MOSS variant has expected regret at most 113 times square root A T plus the largest gap.\[\mathbb E R_T\le 113\sqrt{AT}+\Delta_{\max}.\]Swipe to read the full formula →
Independent rewards supported in [0,1], with the source's anytime index and initialization.
Open primary source ↗
Lower bound
Minimax stochastic-bandit lower bound
Anytime optimal algorithms in stochastic multi-armed bandits
Rémy Degenne and Vianney Perchet · 2016 · Lemma 3
Lower bound guarantee. Formula renderer unavailable; readable fallback: Every policy has a stochastic instance with expected regret at least one twentieth of square root A T under the source's parameter range.\[\inf_\pi\sup_\nu\mathbb E_\nu R_T(\pi)\ge \frac1{20}\sqrt{AT}.\]Swipe to read the full formula →
Use the exact arm-count and horizon restrictions stated in the source.
Open primary source ↗
Local Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Define the anytime MOSS index and measurable generated history policy.
- Prove the same-policy pull-count decomposition and bounded-reward confidence route.
- Compile the matching square-root expected-regret upper terminal without conflating the Gaussian lower class with [0,1] rewards.
formalization frontier
Can the exact anytime MOSS source theorem be compiled on one generated bounded-reward trajectory?
The local Gaussian lower terminal and fixed-horizon MOSS near-minimax theorem compile; the distinct anytime variant remains unformalized.
- Index measurability
- armwise confidence
- pull-count summation
- expected-regret terminal
- Named formalization leaf: MOSS-ANYTIME-GENERATED-UPPER
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
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. Formula renderer unavailable; readable fallback: For every suboptimal Bernoulli arm, KL-UCB's expected pull count has the optimal logarithmic leading constant.\[\limsup_{T\to\infty}\frac{\mathbb E N_a(T)}{\log T}\le\frac1{\mathrm{kl}(\mu_a,\mu_*)}.\]Swipe to read the full formula →
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. Formula renderer unavailable; readable fallback: Every uniformly efficient policy must sample each suboptimal arm at least logarithmically at the information-theoretic rate.\[\liminf_{T\to\infty}\frac{\mathbb E N_a(T)}{\log T}\ge\frac1{\mathrm{kl}(\mu_a,\mu_*)}.\]Swipe to read the full formula →
Use the source's regular parametric-family and efficiency assumptions; the displayed Bernoulli form is a specialization.
Open primary source ↗
Local Lean evidence
Exact declarations
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