Bandit algorithms and proofs of their regret bounds, in Lean.

Useful links:

• Blueprint: a latex document describing the content of the repository, served as html, with links to the code.
• Blueprint as pdf: the same document as a pdf
• Dependency graph: a graph of all definitions and theorems in the project, showing their dependencies
• Doc pages for this repository: documentation of every declaration in the Lean code.
• Zulip chat for Lean: the Lean community chat room. Ask any general Lean or Mathlib question there!