Irrationality Criteria for Series by Erdős and Straus

Title:	Irrationality Criteria for Series by Erdős and Straus
Authors:	Angeliki Koutsoukou-Argyraki and Wenda Li
Submission date:	2020-05-12
Abstract:	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.
BibTeX:	@article{Irrational_Series_Erdos_Straus-AFP, author = {Angeliki Koutsoukou-Argyraki and Wenda Li}, title = {Irrationality Criteria for Series by Erdős and Straus}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{http://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Prime_Distribution_Elementary, Prime_Number_Theorem
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.