BanditRLwiki case · fixed-confidence-best-arm-identification

Fixed-confidence best-arm identification

Track-and-Stop asymptotically matches the characteristic-time change-of-measure lower bound.

← Pure exploration and best-arm identification

Audited comparison

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

best arm identificationTrack-and-Stopdelta-PACstopping timecharacteristic time

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

Aurélien Garivier and Emilie Kaufmann · 2016 · Theorem 14

Upper bound guarantee. Formula renderer unavailable; readable fallback: Track-and-Stop's expected sample complexity approaches alpha times the characteristic time.\[\limsup_{\delta\to0}\frac{\mathbb E_\mu\tau_\delta}{\log(1/\delta)}\le \alpha T^*(\mu).\]

Unique best arm, source exponential-family assumptions, and alpha in the theorem's allowed range.

Open primary source

Lower bound

Characteristic-time lower bound

Optimal Best Arm Identification with Fixed Confidence

Aurélien Garivier and Emilie Kaufmann · 2016 · Theorem 1

Lower bound guarantee. Formula renderer unavailable; readable fallback: Every delta-PAC strategy must spend at least the characteristic-time information cost.\[\mathbb E_\mu\tau_\delta\ge T^*(\mu)\,\mathrm{kl}(\delta,1-\delta),\quad T^*(\mu)^{-1}=\sup_{w\in\Sigma_A}\inf_{\lambda\in\mathrm{Alt}(\mu)}\sum_a w_a d(\mu_a,\lambda_a).\]

The source's alternative set, exponential-family divergence, and stopping/recommendation measurability.

Open primary source

Local 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

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