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

BanditRLwiki case · adversarial-exp3

EXP3 expected regret versus the adversarial minimax rate

Classical EXP3 is near minimax but carries a square-root log A factor relative to the adversarial lower bound.

← Adversarial and best-of-both-worlds bandits

Audited comparison

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
EXP3adversarialexternal regretexpected regretnear minimax
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

Peter Auer, Nicolò Cesa-Bianchi, Yoav Freund, and Robert Schapire · 2002 · EXP3 expected-regret theorem

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 source

Lower bound

Adversarial minimax lower bound

The Nonstochastic Multiarmed Bandit Problem

Peter Auer, Nicolò Cesa-Bianchi, Yoav Freund, and Robert Schapire · 2002 · Section 5 lower bound

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 source

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

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