Let $\delta, \epsilon \in \mathbb{R}$, $\delta >0$, $\epsilon >0$. Let $\{ a_k\}^\infty$,$\{ b_k\}^\infty$ be sequences of positive integers such that

$\lim \sup_{k \rightarrow \infty} \frac{a_{k+1}}{ (\prod^k a_j)^{2 +2/\epsilon + \delta}} \frac{1}{b_{k+1}} = \infty$ and for every suf. large $k$ we have $\sqrt[1+\epsilon]{ \frac{a_{k+1}}{b_{k+1}} }\geq \sqrt[1+\epsilon]{ \frac{a_{k}}{b_{k}} }+1$. Why is the infinite series $\sum^\infty \frac{b_k}{a_k}$ summable? (This claim comes from a theorem in a published paper whose proof we are formalising using the proof assistant Isabelle/HOL. Summability easily follows if we strengthen the assumption substituting $\lim \sup$ with $\lim$, but is there a way to show summability without strengthening any assumption?) Thank you in advance!


The condition that for all large enough $k$ we have $\sqrt[1+\epsilon]{ \frac{a_{k+1}}{b_{k+1}} }\geq \sqrt[1+\epsilon]{ \frac{a_{k}}{b_{k}} }+1$ implies that $\sqrt[1+\epsilon]{ \frac{a_{k}}{b_{k}} }>k-c$ and hence $\frac{b_{k}}{a_{k}}<\frac1{(k-c)^{1+\epsilon}}$ for some real $c>0$ and all large enough $k>c$, which yields the convergence of series $\sum^\infty \frac{b_k}{a_k}$.

(The condition $\lim \sup_{k \rightarrow \infty} \frac{a_{k+1}}{ (\prod^k a_j)^{2 +2/\epsilon + \delta}} \frac{1}{b_{k+1}} = \infty$ is not needed here.)

| cite | improve this answer | |
  • $\begingroup$ Dear Iosif, many thanks - of course your hint will be acknowledged in our code of the formal proof! $\endgroup$ – Angeliki Koutsoukou Argyraki Feb 14 '19 at 23:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.