### 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.

### License

BSD License

### Topics

- Mathematics/Number theory
- Mathematics/Analysis

### Session Irrational_Series_Erdos_Straus

- Irrational_Series_Erdos_Straus

### Depends on

- Elementary Facts About the Distribution of Primes

### Auto-related entries

- Lambert Series

## Cite

×

Irrational_Series_Erdos_Straus-AFP

    @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{https://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 14, 2020 : Isabelle2020
- May 13, 2020 : Isabelle2020