The declarations of Garivier2016Optimal whose docstrings cite a result of the literature, at commit 4f71d11. Each declaration links to the referee site, its file to the source. Declarations in ForLMLExplore/ are the general forms that the project contributes to LMLExplore.
For the headline results, the relation says how the paper’s statement compares with the Lean one, read “paper relation Lean”, as checked against the paper:
- exactMatch: the same claim, up to notation and junk values;
- closeMatch: nearly the same claim, with a difference that a reader should know, such as a convention or a corrected constant;
- broadMatch: the Lean statement is more general;
- narrowMatch: the paper’s statement is more general, for instance when a correction adds a hypothesis;
- hasPart: the Lean statement is one claim of the result.
The same links, in the Literature Links format: annotations.jsonl (28 annotations).
Optimal Best Arm Identification with Fixed Confidence
Aurélien Garivier and Emilie Kaufmann. Proceedings of the 29th Conference on Learning Theory (COLT). 2016. arXiv:1602.04589v2.