mathlib

50fd3d6a - feat(analysis/special_functions/log/monotone): add lemmas (#13848)

feat(analysis/special_functions/log/monotone): add lemmas (#13848) Adds a few lemmas regarding tonality of `log x / x ^ a`, and puts them in a new file, along with previous results.