The goal of this project is to formalize information divergences between probability measures, as well as results about error bounds for (sequential) hypothesis testing.
See the blueprint here: https://remydegenne.github.io/testing-lower-bounds/blueprint/index.html
To do a Mathlib bump without breaking the blueprint, use lake -R -Kenv=dev update