Irrationality Criteria for Series by Erdős and Straus

Angeliki Koutsoukou-Argyraki 🌐 and Wenda Li 🌐

May 12, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalise certain irrationality criteria for infinite series of the form: \[\sum_{n=1}^\infty \frac{b_n}{\prod_{i=1}^n a_i} \] where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers with $a_n >1$ for all large n. The results are due to P. Erdős and E. G. Straus [1]. In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1. The latter is an application of Theorem 2.1 involving the prime numbers.
BSD License


Theories of Irrational_Series_Erdos_Straus