mathlib3

726b7bfd - feat(analysis/specific_limits): a `tfae` about "`f` grows exponentially slower than `R ^ n`" (#5488)

feat(analysis/specific_limits): a `tfae` about "`f` grows exponentially slower than `R ^ n`" (#5488) Also add supporting lemmas here and there. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>