mathlib

41afd8c2 - feat(analysis/special_functions/pow): asymptotics for real powers and log (#14088)

feat(analysis/special_functions/pow): asymptotics for real powers and log (#14088) From the unit fractions project. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>