PatrickMassot/testing-lower-bounds

Lower bounds on testing and estimation, in Lean

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