Commit 2021-06-22 12:45 94a80738

feat(analysis/specific_limits): summability of (λ i, 1 / m ^ f i) (#8023) This PR shows the summability of the series whose ith 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.