mathlib

94a80738 - 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.