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

BanditRLwiki case · nonstationary-best-arm-switch-budget

Unknown best-arm-identity switch budget

ArmSwitch is near the square-root best-arm-switch scale, while the current Lean theorem assumes an oracle schedule built from all global mean changes.

← Delayed and nonstationary bandits

Audited comparison

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
piecewise stationaryswitch budgetArmSwitchchange detectionoracle restart
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

Yasin Abbasi-Yadkori, András György, and Nevena Lazić · 2023 · Theorem 1

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 source

Lower bound

Piecewise-stationary minimax lower bound

A Near-Optimal Change-Detection Based Algorithm for Piecewise-Stationary Combinatorial Semi-Bandits

Zhou, Wang, Varshney, and Lim · 2020 · Theorem 5.1

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 source

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

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