mathlib

e16e093e - feat(analysis/specific_limits): dirichlet and alternating series tests (#11908)

feat(analysis/specific_limits): dirichlet and alternating series tests (#11908) Adds [Dirichlet's test](https://en.wikipedia.org/wiki/Dirichlet%27s_test) along with the [alternating series test](https://en.wikipedia.org/wiki/Alternating_series_test) as a special case of the former. For the curious, [Nick Bingham's course notes](https://www.ma.imperial.ac.uk/~bin06/M2PM3-Complex-Analysis/m2pm3abeldir.pdf) give some more context on Dirichlet's test. It's somewhat obscure. Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Oliver Nash <github@olivernash.org>