Literature
Is the rate matched?
Upper and lower results are compared only after fixing problem class, feedback, horizon, regret notion, probability mode, and salient parameters.
Theorem-level literature comparison
Bound & Source Atlas · BanditRLwiki
Compare published upper and lower bounds only under compatible assumptions, inspect the original theorem/source, then see exactly what BanditRLlib has—and has not—compiled for the same route.
Published optimality, theorem-level source audit, and local Lean compilation are separate ledgers.
7assumption families
13comparison cases
12exact or faithful source audits
0explicit literature-open leaves
2active source-frozen ports outside the comparison atlas
Read three statuses, never one blended badge
Source audit
How precisely was it checked?
An exact theorem audit is different from a normalized rate comparison or a primary reference that still needs theorem-level review.
Lean
What compiles locally?
A compiled dependency or algorithm route is not automatically the paper theorem or a minimax terminal.
Open does not mean missing from this list. “Literature open” appears only after an explicit source audit. “Source audit pending” and “Lean blocked” are separate states.
Compatibility layer · theorem comparison only
Coarse bound-comparison families
These seven families are retained because the existing theorem-level cases are indexed by them. They are not the full Bandit taxonomy. For the long-tail classification—heavy-tailed, causal, combinatorial, quantum, multi-agent, safe, matrix, Lipschitz, GP/RKHS and more—use Bandit Taxonomy.
2 cases
Finite stochastic bandits
Expected, asymptotic, and instance-dependent regret under stationary independent arm rewards.
Open setting → 2 casesAdversarial and best-of-both-worlds bandits
External regret for bounded adversarial losses and algorithms that adapt to stochastic structure.
Open setting → 3 casesLinear and contextual bandits
Linear realizability, self-normalized confidence, finite policy classes, and dimension-dependent lower bounds.
Open setting → 1 caseFinite-horizon tabular reinforcement learning
Episodic tabular MDP regret, Hoeffding and Bernstein bonuses, and full-range minimax behavior.
Open setting → 3 casesDelayed and nonstationary bandits
Delayed observations, variation budgets, switch budgets, dynamic comparators, and adaptive detection.
Open setting → 1 casePure exploration and best-arm identification
Fixed-confidence identification, characteristic time, change of measure, and stopping rules.
Open setting → 1 caseDistributional and high-probability lower bounds
Tail lower bounds, expected-regret tradeoffs, and source-faithful lower-bound proof spines.
Open setting →Legacy anchor · no second taxonomy
Settings and methods moved to canonical views
The old topic-directory anchor is preserved for incoming links. Canonical classification now lives in Bandit Taxonomy; setting→technique relations live in the Technique Map. The ten old topic URLs remain compatibility pages only.
One research system · separate truth contracts
Classification is not a bound, and missing Lean is not an open problem
Bandit Taxonomy
What problem class, objective, feedback, structure or oracle model are we studying?
Technique Map
What new mathematical move handles that changed assumption?
Bound & Source Atlas
This page only: what upper/lower theorem is known, under exactly which assumptions, and where is the original source?
Frontier
Which source-traceable mathematical questions are or were open, and how were they resolved?
Latest repository progress
Active source ports awaiting a matched-bound case
These audits expose real compiled progress, but they are not counted among the 13 upper/lower comparison cases until a theorem-level rate contract and a compatible comparison partner are frozen.
Source-frozen external audit
Succinct stochastic-bandit lower-bound geometry
A Novel General Framework for Sharp Lower Bounds in Succinct Stochastic Bandits
54 named declarations compile in the current library.
Definitions 3.1–3.3, Lemmas 3.1–3.4, the finite-Bessel strict-support route, and a global-R boundedness diagnostic compile.
Boundary. This is a source-frozen partial port, not yet an assumption-matched upper/lower comparison case. Lemmas 3.5–3.6, Assumption 3.7, Theorem 3.8, and every regret endpoint remain uncompiled.
Representative Lean declarations
BanditRL Proof. Lower Bounds. Succinct. Succinct Unit System. source R Set_ not_ bdd Above_ of_ nonzero_ atom_ orthogonal BanditRL Proof. Lower Bounds. Succinct. Succinct Unit System. Is Succinct Support. source Q_ support Combination_ eq BanditRL Proof. Lower Bounds. Succinct. Succinct Unit System. succinct Size_ ge_ strict Size BanditRL Proof. Lower Bounds. Succinct. Succinct Unit System. strictly Succinct Size_ unique
Source-frozen external audit
Stochastic-gradient bandit Theorem 1, Corollary 1, and blocked Theorem-2 follow-on
Does Stochastic Gradient really succeed for Bandits?
361 named declarations compile in the current library.
The counted SGB audit retains the exact 361 = 223 + 23 + 25 + 26 + 7 + 8 + 13 + 28 + 8 audit-slice inventory through one-step selected-reward freshness, terminal-count events, nth-pull-to-count bridges, and a generic finite-horizon low-count regret consumer. A separate ten-declaration native-law module identifies the complete visible/native trajectory law. The selected-block module now has 36 declarations: eight transport finite optimal-arm pull-time/reward blocks to a masked latent-coupling law with explicit `WithTop Nat` missing pulls, fourteen define and transport the exact finite Appendix-C `S0/S1` event, ten split the pure latent phase probability into the generated all-present event plus an explicit missing-pull event, and four map the missing branch to a low-count event, transport its probability to the generated trajectory, and charge its existing mass against expected sampled pseudo-regret. The exact Theorem-1 and Corollary-1 endpoints use generated zero-initialized two-arm fixed-IID trajectories with a Unit Dirac environment prior; the reward laws themselves remain bounded fixed-IID laws. Corollary 1 assumes T >= 2, 0 < Delta < 1, and one fixed eta_T = sqrt(log T / T) per horizon.
Boundary. The audit remains partial. Corollary 1 is a direct Theorem-1 consumer, not evidence for the polynomial-regret Theorem 2. Complete visible/native law equality, missing-pull-aware selected-block transport, exact finite phase-event transport, the disjoint missing/all-present probability split, the missing-pull-to-terminal-count inclusion, and the missing-pull finite-horizon expected-regret consumer now compile. None is a selected-IID theorem or a positive-probability producer. The next unique leaf is the generated all-present Appendix-C phase trigger at a fixed chronological cutoff; the stopped-prefix future-cylinder law, conditional no-return probability >= 1/2, Rademacher/binomial ballot probability, asymptotic assembly, and the frozen terminal remain blocked. Theorem 4 likewise still lacks the general-K generated process, uniform buffer/survival producer, stopped supermartingale/Doob route, and final regret assembly.
Representative Lean declarations
BanditRL Proof. Stochastic Gradient Bandit. softmax Probability_ sum BanditRL Proof. Stochastic Gradient Bandit. expected Source Increment_ eq_ gap Coordinate BanditRL Proof. Stochastic Gradient Bandit. trajectory Measure_ cond Distrib_ next Pair_ given_ environment_ prefix BanditRL Proof. Stochastic Gradient Bandit. integral_ measurable Environment History Step Kernel_ source Increment_ eq_ gap Coordinate BanditRL Proof. Stochastic Gradient Bandit. two Arm Probability At_ zero_ div_ failure_ eq_ exp_ two_ mul BanditRL Proof. Stochastic Gradient Bandit. integral_ exp_ mul_ le_ source Eq Eight_ of_ ae_ abs_ le_ one BanditRL Proof. Stochastic Gradient Bandit. integral_ measurable Environment History Step Kernel_ exp_ action Reward_ le_ source Eq Eight_ of_ mean BanditRL Proof. Stochastic Gradient Bandit. integral_ two Arm History Step Kernel_ exp_ forward Successor_ le_ add_ success_ sq BanditRL Proof. Stochastic Gradient Bandit. integral_ two Arm Initial Pair Kernel_ exp_ inverse Increment_ le BanditRL Proof. Stochastic Gradient Bandit. Two Arm Bounded Fixed Mean Environment Contract BanditRL Proof. Stochastic Gradient Bandit. trajectory Prefix_ cond Distrib_ integral_ forward Successor_ le BanditRL Proof. Stochastic Gradient Bandit. integrable_ two Arm Forward Trajectory Successor Potential BanditRL Proof. Stochastic Gradient Bandit. two Arm Forward Trajectory Successor_ cond Exp_ le_ recurrence Bound BanditRL Proof. Stochastic Gradient Bandit. integrable_ measurable Two Arm History Step Kernel_ source Increment_ of_ contract BanditRL Proof. Stochastic Gradient Bandit. two Arm Fixed IID Environment_ contract BanditRL Proof. Stochastic Gradient Bandit. integral_ two Arm Fixed IID History Step Kernel_ source Increment_ eq_ gap Coordinate BanditRL Proof. Stochastic Gradient Bandit. two Arm Forward Unconditional Recurrence BanditRL Proof. Stochastic Gradient Bandit. two Arm Inverse Failure Mass Sq Telescope BanditRL Proof. Stochastic Gradient Bandit. two Arm Full Failure Mass Sq Sum_ le BanditRL Proof. Stochastic Gradient Bandit. integral_ two Arm Sampled Pseudo Regret_ eq_ generated BanditRL Proof. Stochastic Gradient Bandit. integral_ two Arm Sampled Pseudo Regret_ le_ source Theorem One BanditRL Proof. Stochastic Gradient Bandit. two Arm Fixed IID Dirac_ theorem One BanditRL Proof. Stochastic Gradient Bandit. two Arm Fixed IID Dirac_ corollary One BanditRL Proof. Stochastic Gradient Bandit. two Arm Nth Optimal Pull Time_ spec BanditRL Proof. Stochastic Gradient Bandit. measurable_ two Arm Nth Optimal Pull Reward BanditRL Proof. Stochastic Gradient Bandit. measurable_ two Arm Nth Optimal Pull Success Probability BanditRL Proof. Stochastic Gradient Bandit. two Arm Fixed IID Latent Trajectory Measure_ map_ optimal Prefix_ eq_ pi BanditRL Proof. Stochastic Gradient Bandit. two Arm Nth Optimal Pull Reward_ eq_ latent Coordinate_ ae BanditRL Proof. UCB. arm Stream Measure_ map_ frestrict Le_ eq_ pi BanditRL Proof. Thompson. latent Arm Stream Trajectory Kernel_ map_ frestrict Le_ eq_ of_ stream Prefix_ eq BanditRL Proof. Thompson. latent Arm Stream Trajectory Measure_ map_ stream_ visible Prefix_ eq BanditRL Proof. Thompson. latent Arm Stream Trajectory Measure_ map_ visible Prefix_ next Action_ eq_ comp Prod BanditRL Proof. Thompson. latent Arm Stream Visible Next Reward_ eq_ selected Coordinate_ ae BanditRL Proof. Thompson. latent Arm Stream Visible Prefix Next Action_ coordinate_ branch_ eq_ prod_ of_ locality BanditRL Proof. Thompson. latent Arm Stream Visible Prefix Next Action_ coordinate_ branch_ eq_ prod BanditRL Proof. Thompson. latent Arm Stream Visible Next Reward_ joint_ eq_ comp Prod BanditRL Proof. Thompson. latent Arm Stream Visible Next Reward_ cond Distrib_ ae_ eq_ nu BanditRL Proof. Thompson. latent Arm Stream Visible Trajectory Measure_ next Reward_ cond Distrib_ ae_ eq_ nu BanditRL Proof. Thompson. real History Pull Count_ extend Pair History Succ BanditRL Proof. Stochastic Gradient Bandit. two Arm Optimal Pull Count Below Event_ charge_ mul_ probability_ le_ integral BanditRL Proof. Stochastic Gradient Bandit. two Arm Fixed IID Step One Starvation Event_ charge_ mul_ probability_ le_ integral BanditRL Proof. Stochastic Gradient Bandit. theorem Four Step One Margin_ pos BanditRL Proof. Stochastic Gradient Bandit. theorem Four Step Four_ survival Mass_ pos BanditRL Proof. Stochastic Gradient Bandit. theorem Four Finite Transient Mass_ le_ inv
Upper · lower · Lean
All comparison cases
13 matching 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
Open stable case page →Faithful restatement
- 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
Upper bound guarantee. The anytime MOSS variant has expected regret at most 113 times square root A T plus the largest gap.
Independent rewards supported in [0,1], with the source's anytime index and initialization.
Open primary sourceLower bound
Minimax stochastic-bandit lower bound
Anytime optimal algorithms in stochastic multi-armed bandits
Lower bound guarantee. Every policy has a stochastic instance with expected regret at least one twentieth of square root A T under the source's parameter range.
Use the exact arm-count and horizon restrictions stated in the source.
Open primary sourceLocal 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
Open stable case page →Faithful restatement
- 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
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 sourceLower bound
Lai–Robbins asymptotic information lower bound
Asymptotically Efficient Adaptive Allocation Rules
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 sourceLocal 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
adversarial-exp3 EXP3 expected regret versus the adversarial minimax rateClassical EXP3 is near minimax but carries a square-root log A factor relative to the adversarial lower bound. Near minimaxPartial local route
Open stable case page →Faithful restatement
- Loss model
- Oblivious or predictable losses in [0,1]
- Feedback
- Selected-action bandit loss
- Regret
- Expected external regret to the best fixed action
- Target scale
- sqrt(A T)
Comparison judgment
Near minimax
The source contains both the EXP3 upper route and an adversarial lower bound. The local generated expected EXP3 endpoint compiles.
Known gap. EXP3 has a multiplicative square-root log A gap; removing it requires a different regularizer such as INF/Tsallis-INF, not a relabeling of EXP3.
Local Lean boundary
Partial local route
The generated predictable EXP3 process compiles an explicit 4 sqrt(A T log A) expected bound under its tuning condition, together with several separately scoped tail routes. The adversarial minimax lower terminal is not compiled.
Upper bound
EXP3 expected-regret upper bound
The Nonstochastic Multiarmed Bandit Problem
Upper bound guarantee. EXP3 achieves expected regret of order square root A T log A against bounded adversarial rewards.
Finite actions and the source's learning-rate tuning.
Open primary sourceLower bound
Adversarial minimax lower bound
The Nonstochastic Multiarmed Bandit Problem
Lower bound guarantee. Every bandit algorithm suffers expected regret of order at least square root A T on some adversarial loss sequence.
Finite actions under the source's horizon range.
Open primary sourceLocal Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Pair the corrected high-probability lower terminal with the upper route under one exact regret contract.
- Keep fixed-horizon, all-positive-prefix, and horizon-free tuning contracts distinct.
- Use a minimax-optimal algorithm route if the log A factor is to be removed.
formalization frontier
Can the local adversarial upper route be paired with a compiled minimax lower terminal under one exact regret contract?
The EXP3 upper compiles; corrected Chapter 17 Theorem 17.4 now passes focused compilation with δ ≤ 1/32, c=1/160 and C=64; full local gates pass.
- matched upper/lower regret contract; corrected Chapter 17 high-probability construction is compiled
- Named formalization leaf: CH17-CLIPPED-NORMAL-LAW
- Named formalization leaf: CH17-CLAIM-17-6
- Named formalization leaf: CH17-CLAIM-17-7
- Named formalization leaf: CH17-THM-17-4
adversarial-stochastic-best-of-both-worlds Tsallis-INF best of stochastic and adversarial worldsOne Tsallis-INF algorithm attains the adversarial square-root rate and stochastic gap-dependent logarithmic regret. Near minimaxPartial local route
Open stable case page →Faithful restatement
- Loss model
- Bounded adversarial losses or a stochastic/self-bounding gap condition
- Algorithm identity
- The same Tsallis-INF estimator and scheduler across regimes
- Regret
- Expected pseudo-regret/external regret as stated by the source
- Target scales
- sqrt(A T) adversarial and sum log(T)/Delta_a stochastic
Comparison judgment
Near minimax
The source theorem is genuinely best-of-both-worlds at the displayed rate scale. This card does not claim asymptotic instance optimality or an exact stochastic information constant; the local paper-identity and unified paired terminal remain open.
Known gap. The adversarial branch is minimax-rate optimal within universal constants, while the self-bounding stochastic branch is gap-log rate optimal within constants and is not an exact Lai–Robbins leading-constant result. The local routes also lack identity with the paper's single algorithm across both regimes.
Local Lean boundary
Partial local route
BanditRLlib compiles half-Tsallis IID logarithmic, corruption, drifting-mean, and oracle-restart terminals. It does not claim that one local generated policy is definitionally the paper algorithm with both optimal source guarantees.
Upper bound
Tsallis-INF best-of-both-worlds upper bounds
Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits
Upper bound guarantee. The same Tsallis-INF construction has a minimax-order adversarial bound and a logarithmic gap-dependent stochastic bound.
The exact constants and lower-order terms depend on the importance-weighted or reduced-variance estimator variant.
Open primary sourceLower bound
Rate-optimality comparison used by the Tsallis-INF analysis
Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits
Lower bound guarantee. The adversarial minimax and stochastic information lower bounds supply the comparison scales used by the source.
The stochastic lower constant is model dependent; do not identify a generic gap-only upper with the exact Bernoulli information constant.
Open primary sourceLocal Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Prove the exact estimator, regularizer, and learning-rate identity with the source algorithm.
- Package the stochastic and adversarial guarantees for the same generated policy.
- Audit paper-sharp constants and high-probability or realized-regret variants separately.
formalization frontier
Can one local generated half-Tsallis policy be shown identical to paper Tsallis-INF and carry both source guarantees?
Several strong local endpoints compile, but they are not yet a unified source-identity theorem.
- Estimator identity
- scheduler identity
- same-policy paired theorem
- constant audit
- Named formalization leaf: TSALLIS-INF-PAPER-IDENTITY
- Named formalization leaf: TSALLIS-INF-SAME-POLICY-BOBW
contextual-finite-policy-exp4p Finite-policy contextual bandits with Exp4.PExp4.P gives high-probability policy regret for a finite expert class; the exact matching lower source still needs theorem-level audit in this Wiki. Source audit pendingPlanned
Open stable case page →Primary reference pending
- Context model
- Adversarial contexts and rewards
- Policy class
- N finite experts mapping contexts to A actions
- Regret
- High-probability regret to the best policy
- Target scale
- sqrt(A T log(N/delta))
Comparison judgment
Source audit pending
This is a source-audit queue item, not a claim that the lower bound is unknown in the literature.
Known gap. The upper theorem is indexed exactly; a compatible primary lower theorem, assumptions, and constants have not yet been frozen here.
Local Lean boundary
Planned
No finite-policy contextual Exp4.P terminal is mapped to a local Lean declaration.
Upper bound
Exp4.P high-probability policy-regret upper bound
Contextual Bandit Algorithms with Supervised Learning Guarantees
Upper bound guarantee. Exp4.P has high-probability regret at most six times square root A T log N over delta under the source conditions.
Includes the source's uniform expert and log(N/delta) at most A T conditions.
Open primary sourceLower bound
No source theorem claimed
The source audit has not registered a compatible theorem for this side of the comparison.
Local Lean evidence
Exact declarations
- No local declaration is claimed for this target.
Not yet proved here
Missing steps
- Define measurable context-to-action experts and the expert-mixture sampler.
- Formalize the importance-weighted estimator and Exp4.P variance bonus.
- Audit and freeze the exact compatible lower theorem before assigning near-minimax status.
formalization frontier
Which exact contextual lower theorem matches the displayed Exp4.P contract, and how should its policy class be represented in Lean?
The Exp4.P upper theorem is frozen; the lower-source audit and all local formalization remain pending.
- Exact lower source
- expert measurability
- mixture action law
- high-probability terminal
- Named formalization leaf: EXP4P-LOWER-SOURCE-AUDIT
- Named formalization leaf: EXP4P-CONTEXT-POLICY-INTERFACE
stochastic-linear-oful Stochastic linear bandits: OFUL versus dimension-dependent lower boundsOFUL is near minimax up to logarithmic factors in dimension-dependent high-probability regret. Near minimaxPartial local route
Open stable case page →Exact source theorem
- Reward model
- Linear mean x_t dot theta-star with conditionally sub-Gaussian noise
- Geometry
- Bounded actions and parameter norm in dimension d
- Regret
- High-probability cumulative pseudo-regret
- Target scale
- d sqrt(T) up to logarithmic factors
Comparison judgment
Near minimax
The upper and lower dimension dependence agree at leading polynomial order. The local route is a finite-action scalar-ridge specialization, not the full paper theorem.
Known gap. Logarithmic factors, source normalization, decision-set generality, and constants separate the OFUL upper from the d sqrt(T) lower. The displayed upper is high probability, whereas the lower is an expected-regret minimax statement, so the comparison is only at leading polynomial scale.
Local Lean boundary
Partial local route
Elliptical potential, self-normalized ridge confidence, a measurable horizon-free finite-action policy, all-time confidence, and one-policy all-horizon regret compile. Full source geometry and the linear lower bound do not.
Upper bound
OFUL high-probability regret upper bound
Improved Algorithms for Linear Stochastic Bandits
Upper bound guarantee. OFUL has a high-probability dimension times square root T regret bound up to logarithmic and regularization factors.
Use the exact confidence radius, determinant term, action-set, and norm assumptions in Theorem 13.
Open primary sourceLower bound
Linear-bandit minimax expected-regret lower bound
Stochastic Linear Optimization under Bandit Feedback
Lower bound guarantee. A constructed linear decision domain forces expected regret at least one tenth d square root T.
The lower theorem uses its explicit domain, dimension, and horizon range.
Open primary sourceLocal Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Audit exact correspondence with OFUL Theorem 13 constants and normalization.
- Generalize beyond the current finite-action scalar-ridge interface.
- Formalize a compatible Gaussian linear hard family and d sqrt(T) lower terminal.
formalization frontier
Can the finite-action scalar route be lifted to the exact OFUL theorem and paired with a compatible linear minimax lower construction?
The local high-probability all-horizon consumer is strong but intentionally narrower than the source theorem.
- General decision set
- source radius identity
- hard family
- upper/lower comparison terminal
- Named formalization leaf: OFUL-SOURCE-THEOREM-13-IDENTITY
- Named formalization leaf: LINEAR-BANDIT-MINIMAX-LOWER
finite-action-linear-contextual Finite-action linear contextual minimax ratesSupLinUCB/VCL upper and lower theorems match the finite-action contextual rate up to iterated logarithms. Near minimaxPlanned
Open stable case page →Exact source theorem
- Context model
- d-dimensional realizable contexts with n available actions per round
- Reward model
- Stochastic linear reward
- Regret
- Expected cumulative regret
- Target scale
- square root(d T log T log n), up to iterated logarithms
Comparison judgment
Near minimax
The source gives both sides under an explicit parameter fence. Do not treat the local OFUL scaffold as a proof of this contextual finite-action result.
Known gap. The upper differs from the lower by iterated logarithms; Theorem 2 also requires n at most 2^(d/2) and T at least d (log_2 n)^(1+epsilon).
Local Lean boundary
Planned
No time-varying finite-action contextual theorem is claimed locally. Existing OFUL declarations are reusable proof infrastructure only.
Upper bound
Finite-action linear contextual upper bound
Nearly Minimax-Optimal Regret for Linearly Parameterized Bandits
Upper bound guarantee. The minimax regret is at most square root d T log T log n times iterated-logarithmic factors.
Finite action sets and the source's realizability, action-count, dimension, and horizon conditions.
Open primary sourceLower bound
Finite-action linear contextual lower bound
Nearly Minimax-Optimal Regret for Linearly Parameterized Bandits
Lower bound guarantee. Under the theorem's action-count and horizon fence, every algorithm has regret at the displayed finite-action contextual scale.
For every small epsilon greater than zero, n is at most 2^(d/2) and T is at least d (log_2 n)^(1+epsilon), together with the source's remaining conditions.
Open primary sourceLocal Lean evidence
Exact declarations
- No local declaration is claimed for this target.
Not yet proved here
Missing steps
- Represent time-varying action sets and contexts measurably.
- Formalize the VCL layer partition and contextual lower construction.
- Retain the action-count and horizon fence in the final comparison theorem.
formalization frontier
Can the exact Theorems 1–2 parameter fence and VCL construction be represented in one contextual Lean history law?
The primary upper/lower comparison is audited; all local contextual algorithm and lower-construction work remains planned.
- Contextual history law
- VCL layers
- parameter fence
- lower construction
- Named formalization leaf: VCL-CONTEXTUAL-HISTORY-LAW
- Named formalization leaf: VCL-LAYER-PARTITION
- Named formalization leaf: VCL-LOWER-CONSTRUCTION
tabular-finite-horizon-rl-ucbvi Tabular finite-horizon RL: UCBVI and minimax leading ratesUCBVI-BF has the near-minimax variance-aware leading rate; BanditRLlib currently compiles the known-reward Hoeffding UCBVI-CH terminal. Near minimaxPartial local route
Open stable case page →Faithful restatement
- MDP
- Unknown episodic tabular transitions with S states, A actions, horizon H
- Episodes
- K episodes and total steps T=H K
- Regret
- High-probability cumulative episode pseudo-regret
- Target scale
- square root(H S A T), plus lower-order terms
Comparison judgment
Near minimax
The literature and local status must be read separately: UCBVI-CH compiles locally, while the variance-aware source-leading theorem does not.
Known gap. UCBVI-BF gives a high-probability upper bound whose leading large-T polynomial rate matches the expected-regret minimax lower scale up to logs and lower-order terms; these probability modes are not identical theorem contracts. A later modified MVP route addresses the full parameter range. The compiled local theorem is Hoeffding, not Bernstein/minimax.
Local Lean boundary
Partial local route
The canonical recurrent known-reward Hoeffding UCBVI-CH 20/250 high-probability terminal and failure-aware expected consumer compile. Bernstein/Freedman, stochastic rewards, and a minimax lower pair do not.
Upper bound
UCBVI high-probability regret upper bounds
Minimax Regret Bounds for Reinforcement Learning
Upper bound guarantee. The Hoeffding version has the explicit 20 and 250 bound; the Bernstein-Freedman version improves the leading horizon dependence to the near-minimax scale.
Use the paper's confidence logarithm L, reward model, and horizon conditions.
Open primary sourceUpper bound
Modified MVP full-range minimax regret bound
Settling the sample complexity of online reinforcement learning
Upper bound guarantee. A modified MVP analysis supplies the closest full-range upper guarantee across all episode counts.
This is a separate algorithmic route and must not be relabeled as UCBVI.
Open primary sourceLower bound
Tabular episodic minimax lower-bound comparison
Minimax Regret Bounds for Reinforcement Learning
Lower bound guarantee. Some tabular finite-horizon MDP forces expected regret at the square-root H S A T scale in the source regime.
Use the source's state, action, horizon, and total-time range.
Open primary sourceLocal Lean evidence
Exact declarations
BanditRL Proof. Finite Horizon RL. Adaptive Cumulative Hoeffding UCBVI. recurrent Source_ trajectory Measure_ cumulative Episode Pseudo Regret_ gt_ canonical Regret Bound_ le BanditRL Proof. Finite Horizon RL. Adaptive Cumulative Hoeffding UCBVI. integral_ cumulative Episode Pseudo Regret_ recurrent Source_ le_ canonical Regret Bound_ add_ failure
Not yet proved here
Missing steps
- Build the conditional variance and Freedman/Bernstein bonus layer.
- Compile the law-of-total-variance and recurrent value/Q recursion needed by UCBVI-BF.
- Treat stochastic rewards, realized sampled-return regret, and the MVP full-range route as distinct extensions.
formalization frontier
Can the recurrent generated UCBVI source be upgraded from Hoeffding bonuses to the exact Bernstein/Freedman source theorem?
The source-shaped UCBVI-CH endpoint compiles with the exact 20/250 surface; the minimax-leading UCBVI-BF route is absent.
- Conditional variance
- Freedman concentration
- variance bonus summation
- source-leading terminal
- Named formalization leaf: UCBVI-BF-CONDITIONAL-VARIANCE
- Named formalization leaf: UCBVI-BF-TOTAL-VARIANCE
- Named formalization leaf: UCBVI-BF-TERMINAL
delayed-adversarial-bandit Adversarial bandits with delayed feedbackKnown-delay algorithms attain square-root dependence on rounds and total delay up to logs; local work currently compiles accounting and source-audit interfaces, not a regret endpoint. Near minimaxPartial local route
Open stable case page →Faithful restatement
- Loss model
- Adversarial bounded losses
- Delay model
- Per-round delays d_t with total D, or a fixed delay d
- Regret
- Expected external regret
- Target scale
- sqrt((A T + D) log A), with fixed-delay variants
Comparison judgment
Near minimax
The literature has strong delayed-feedback rates. Local declarations prove causal views and accounting identities but not the cited algorithm theorem.
Known gap. Logarithmic factors and the distinction between total-delay and fixed-delay contracts remain visible.
Local Lean boundary
Partial local route
Observed/outstanding partition identities, causal action-time views, active allocation, a nonnegative-domain D.11 core, Algorithm-5 line-10 eliminated-arm initialization, and several Delayed SAPO audit surfaces compile. The central generated delayed process and stochastic/adversarial regret endpoints do not.
Upper bound
Known-delay DEXP3/DEW upper bound
Nonstochastic Multiarmed Bandits with Unrestricted Delays
Upper bound guarantee. A delayed exponential-weights algorithm has expected regret controlled by the sum of the ordinary bandit term and total delay.
Use the source's known-delay or skipping contracts and parameter choice.
Open primary sourceUpper bound
Fixed-delay regret upper bound
Delay and Cooperation in Nonstochastic Bandits
Upper bound guarantee. For fixed delay d, the regret is square-root in A plus d times T, up to log A and an additive delay term.
Fixed-delay feedback under the source's protocol.
Open primary sourceLower bound
Fixed-delay minimax comparison
Delay and Cooperation in Nonstochastic Bandits
Lower bound guarantee. The fixed-delay problem has a square-root lower scale in A plus delay times T.
Compare only to upper theorems with the same fixed-delay feedback contract.
Open primary sourceLocal Lean evidence
Exact declarations
BanditRL Proof. Delayed Feedback. card_ observed Before_ add_ card_ outstanding At BanditRL Proof. Delayed Feedback. action Time View At BanditRL Proof. Delayed Feedback. delayed SAPO Probability BanditRL Proof. Delayed Feedback. two_ mul_ card_ source Stochastic Loss Gap_ above Twice Average_ le BanditRL Proof. Delayed Feedback. Delayed SAPO Eliminated Arm Initialization. initialize Newly Eliminated_ spec_ of_ mem
Not yet proved here
Missing steps
- Extend the line-10 initializer into the source EAP/BSC phase transitions and one recursive delayed trajectory that supports out-of-order feedback revelation.
- Resolve the source width-direction audit and instantiate its snapshot hypotheses.
- Prove a source-compatible stochastic or adversarial regret terminal.
formalization frontier
Can the delayed accounting layer be connected to one generated algorithm law and a paper-level regret terminal?
The bookkeeping, causal-view, active-allocation, and conditional source-audit surfaces compile; no algorithm regret theorem is claimed.
- Out-of-order reveal law
- state machine
- width audit
- regret terminal
- Named formalization leaf: DELAYED-TRAJECTORY-LAW
- Named formalization leaf: DELAYED-SAPO-D10-D12
- Named formalization leaf: DELAYED-REGRET-TERMINAL
nonstationary-variation-budget Variation-budget nonstationary stochastic banditsRestarted EXP3 is near minimax for dynamic regret under a known total-variation budget. Near minimaxPartial local route
Open stable case page →Exact source theorem
- Reward model
- Time-varying stochastic arm means
- Variation
- V_T equals the sum of roundwise maximum mean changes
- Comparator
- Roundwise best arm dynamic oracle
- Target scale
- (A V_T)^(1/3) T^(2/3)
Comparison judgment
Near minimax
The published upper and lower exponents match. The local drifting-mean Tsallis theorem is related but is not the V_T minimax theorem.
Known gap. Rexp3 has a (log A)^(1/3) factor and assumes variation-budget tuning.
Local Lean boundary
Partial local route
A drifting-mean half-Tsallis dynamic-regret envelope compiles, but it is not a formal variation-budget Rexp3 theorem and does not close the minimax comparison.
Upper bound
Rexp3 variation-budget upper bound
Stochastic Multi-Armed-Bandit Problem with Non-stationary Rewards
Upper bound guarantee. Rexp3 has dynamic regret of order cube root A log A times variation, multiplied by T to the two thirds.
The block length uses the source's known variation budget and parameter range.
Open primary sourceLower bound
Variation-budget dynamic-regret lower bound
Stochastic Multi-Armed-Bandit Problem with Non-stationary Rewards
Lower bound guarantee. Every policy incurs dynamic regret at the cube-root variation-budget scale on some admissible nonstationary environment.
Use the source's variation class and horizon/variation range.
Open primary sourceLocal Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Define the formal variation budget and block restart policy.
- Prove the dynamic-oracle decomposition for Rexp3.
- Optimize the block length and compile the matching V_T rate.
formalization frontier
Can the current dynamic-regret envelope be specialized to the exact variation-budget Rexp3 theorem?
A related drifting-mean theorem compiles, but its contract and rate are not the source minimax V_T result.
- Variation measure
- restart construction
- oracle decomposition
- rate optimization
- Named formalization leaf: VARIATION-BUDGET-DEFINITION
- Named formalization leaf: REXP3-BLOCK-RESTART
- Named formalization leaf: REXP3-DYNAMIC-REGRET
nonstationary-best-arm-switch-budget Unknown best-arm-identity switch budgetArmSwitch is near the square-root best-arm-switch scale, while the current Lean theorem assumes an oracle schedule built from all global mean changes. Near minimaxPartial local route
Open stable case page →Faithful restatement
- Reward model
- Nonstationary stochastic means
- Changes
- The identity of the optimal arm changes at most S times, unknown to the learner
- Comparator
- Best arm within each stationary segment
- Target scale
- sqrt(A (S+1) T) up to polylogarithmic factors
Comparison judgment
Near minimax
The upper depends on changes in best-arm identity, not changes in the full reward vector. The local oracle schedule uses every global population-mean change and is therefore only related evidence.
Known gap. ArmSwitch has a polylogarithmic factor. The displayed lower is obtained from a stationary-segment hard family, so the class embedding and its K/horizon conditions remain explicit rather than being called an identical assumption contract.
Local Lean boundary
Partial local route
A generated oracle-restart half-Tsallis theorem with 8 sqrt(A) sqrt(S+1) sqrt(T+1) compiles, but its S counts true global population-mean changes, not only changes in best-arm identity.
Upper bound
ArmSwitch best-arm-switch upper bound
A New Look at Dynamic Regret for Non-Stationary Stochastic Bandits
Upper bound guarantee. ArmSwitch adapts to an unknown number of changes with square-root switch dependence up to a polylogarithmic factor.
Use the source's piecewise-stationary model and initialization.
Open primary sourceLower bound
Piecewise-stationary minimax lower bound
A Near-Optimal Change-Detection Based Algorithm for Piecewise-Stationary Combinatorial Semi-Bandits
Lower bound guarantee. A piecewise-stationary hard family with N segments forces square-root N A T regret; ordinary multi-armed bandits are a special case of the source model.
Use the theorem's A at least 3 and horizon conditions. Mapping N segments to S plus one best-arm regimes is a faithful comparison step, not a verbatim identity of model classes.
Open primary sourceLocal Lean evidence
Exact declarations
Not yet proved here
Missing steps
- Define a measurable observed-reward change detector and adaptive restart state.
- Control detection delay and false alarms before claiming the unknown-S rate.
- Bridge—or explicitly separate—the best-arm-identity switch contract from the local global-mean-change schedule.
formalization frontier
Can oracle global-mean restarts be replaced by an observed-reward detector under the broader best-arm-identity switch contract?
The local theorem has the desired square-root expression only under a true global-change schedule; ArmSwitch is adaptive under a different, broader change count.
- Assumption bridge
- detector measurability
- false-alarm control
- delay charge
- Named formalization leaf: BEST-ARM-SWITCH-CONTRACT
- Named formalization leaf: OBSERVED-CHANGE-DETECTOR
- Named formalization leaf: ADAPTIVE-RESTART-REGRET
fixed-confidence-best-arm-identification Fixed-confidence best-arm identificationTrack-and-Stop asymptotically matches the characteristic-time change-of-measure lower bound. Asymptotically matchedPlanned
Open stable case page →Exact source theorem
- Reward model
- One-parameter exponential family with a unique best arm
- Guarantee
- delta-PAC best-arm recommendation
- Cost
- Expected stopping time as delta tends to zero
- Target constant
- Characteristic time T-star of the max-min information game
Comparison judgment
Asymptotically matched
The literature has a matched asymptotic fixed-confidence answer. BanditRLlib has no characteristic-time or Track-and-Stop formalization yet.
Known gap. The source's tracking parameter alpha is in [1,e/2]; appropriate tuning approaches the characteristic-time constant.
Local Lean boundary
Planned
No delta-PAC stopping-time characteristic-time terminal or Track-and-Stop algorithm is claimed locally.
Upper bound
Track-and-Stop asymptotic upper bound
Optimal Best Arm Identification with Fixed Confidence
Upper bound guarantee. Track-and-Stop's expected sample complexity approaches alpha times the characteristic time.
Unique best arm, source exponential-family assumptions, and alpha in the theorem's allowed range.
Open primary sourceLower bound
Characteristic-time lower bound
Optimal Best Arm Identification with Fixed Confidence
Lower bound guarantee. Every delta-PAC strategy must spend at least the characteristic-time information cost.
The source's alternative set, exponential-family divergence, and stopping/recommendation measurability.
Open primary sourceLocal Lean evidence
Exact declarations
- No local declaration is claimed for this target.
Not yet proved here
Missing steps
- Define delta-PAC recommendation and the adapted stopping rule.
- Formalize the stopped change-of-measure inequality.
- Build the simplex max-min characteristic time and the Track-and-Stop tracking/concentration proof.
formalization frontier
How should the characteristic-time max-min game and an unbounded adaptive stopping rule be represented in Lean?
General stopping-time infrastructure exists elsewhere in BanditRLlib, but no pure-exploration semantic bridge or source theorem is mapped.
- Recommendation event
- stopping measurability
- information game
- tracking rule
- Named formalization leaf: BAI-DELTA-PAC
- Named formalization leaf: BAI-STOPPED-CHANGE-OF-MEASURE
- Named formalization leaf: BAI-CHARACTERISTIC-TIME
- Named formalization leaf: TRACK-AND-STOP
distributional-high-probability-regret Distributional high-probability regret under an expected-regret constraintA 2026 upper theorem matches the Chapter 17 logarithmic confidence tradeoff in order. Theorem 17.1, Corollaries 17.2–17.3, and the explicitly corrected adversarial terminal pass the full local repository gate. EQO+ remains a separate unformalized upper route. Minimax matchedPartial local route
Open stable case page →Exact source theorem
- Reward model
- Finite stochastic sub-Gaussian or unit-Gaussian arms
- Policy premise
- Uniform expected regret of order B sqrt((A-1) T) for the lower theorem
- Regret
- Tail of random pseudo-regret
- Target scale
- sqrt(A T) log(1/delta), capped by T
Comparison judgment
Minimax matched
This literature frontier is closed by the 2026 EQO+ result. Chapter 17's stochastic endpoints compile, and corrected Theorem 17.4 passes focused compilation on 0 < δ ≤ 1/32 with c=1/160, C=64. Full local gates pass; this does not formalize EQO+.
Known gap. The upper and lower tradeoff match in confidence and square-root order, with constants, exact reward class, and the lower theorem's expected-regret premise remaining visible.
Local Lean boundary
Partial local route
BanditRLlib compiles the stochastic Chapter 17 endpoints, Claims 17.5–17.7, Eq. (17.8), same-policy shared-noise coupling, and deterministic matrix extraction. Approved corrections: Claim 17.6 uses T_i ≤ n/2; Theorem 17.4 uses 0 < δ ≤ 1/32, c=1/160, C=64 and a strict CDF tail. The full local repository gate passes; EQO+ is not formalized.
Upper bound
EQO+ distributional-regret upper bound
Unified Framework of Distributional Regret in Multi-Armed Bandits and Reinforcement Learning
Upper bound guarantee. EQO+ simultaneously controls expected regret at the minimax scale and the distributional tail with one logarithmic confidence factor.
Use the source's sub-Gaussian model and its displayed tuning c1 equals sigma square root T over A.
Open primary sourceLower bound
Chapter 17 distributional-regret lower bound
Bandit Algorithms
Lower bound guarantee. Any policy with the source's uniform expected-regret bound has a unit-Gaussian instance whose random pseudo-regret exceeds the displayed confidence-dependent threshold with probability at least delta.
Preserve the exact A, T, B, delta conditions and the same randomized nonanticipating policy.
Open primary sourceLocal Lean evidence
Exact declarations
BanditRL Proof. Lower Bounds. stochastic High Probability Threshold BanditRL Proof. Lower Bounds. gaussian Random Pseudo Regret_ ge_ theorem17_ 1 BanditRL Proof. Lower Bounds. no Uniform Gaussian Random Pseudo Regret Tail_ corollary17_ 3 BanditRL Proof. Lower Bounds. gaussian Random Pseudo Regret_ ge_ corollary17_ 2 BanditRL Proof. Lower Bounds. exists_ cdf Tail_ ge_ of_ integral_ ge BanditRL Proof. Lower Bounds. random Regret_ ge_ quarter_ of_ clipping Decomposition BanditRL Proof. Lower Bounds. adversarial Random Regret_ ge_ eq17_ 8
Not yet proved here
Missing steps
- Map and formalize the EQO+ algorithm and Theorem 4 as a separate upper route.
formalization frontier
Can the compiled corrected lower terminal be paired with a formalized EQO+ upper route?
Theorem 17.1, Corollaries 17.2–17.3, Eq. (17.8), corrected Claim 17.6, exact Claim 17.7, and corrected Theorem 17.4 pass the full local repository gate. Theorem 17.4 uses 0 < δ ≤ 1/32, c=1/160, C=64. No EQO+ algorithm theorem is claimed.
- EQO+ source map and formalized upper terminal
- Named formalization leaf: CH17-HISTORY-INFORMATION
- Named formalization leaf: CH17-THEOREM-17-1
- Named formalization leaf: CH17-COROLLARY-17-2
- Named formalization leaf: CH17-COROLLARY-17-3
- Named formalization leaf: EQOPLUS-UPPER