feat(analysis/specific_limits): summability of `(λ i, 1 / m ^ f i)` (#8023)
feat(analysis/specific_limits): summability of `(λ i, 1 / m ^ f i)` (#8023)

This PR shows the summability of the series whose `i`th term is `1 / m ^ f i`, where `1 < m` is a fixed real number and `f : ℕ → ℕ` is a function bounded below by the identity function.  While a function eventually bounded below by a constant at least equal to 2 would have been enough, this specific shape is convenient for the Liouville application.

I extracted this lemma, following the discussion in PR #8001.





leanprover-community/mathlib,leanprover-community/mathlib