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