LeanBandits

1 Introduction
2 Iterative stochastic algorithms ▶
- 2.1 Ionescu-Tulcea theorem ▶
  - Case of a composition-product
- 2.2 Independence and Markov property
3 Stochastic multi-armed bandits ▶
4 Concentration inequalities
5 Bandit algorithms ▶
- 5.1 Explore-Then-Commit
- 5.2 UCB
6 Practical Algorithms ▶
- Alternative strategy: atomic typeclasses
- Error sensitivity analysis
7 Sampling
8 Bibliography
Dependency graph

Bibliography

Mar25: Etienne Marion, A formalization of the ionescu-tulcea theorem in mathlib, arXiv preprint arXiv:2506.18616 (2025).