# 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