[isabelle] New in the AFP: Irrationality Criteria for Series by Erdős and Straus



Dear all,

AFP-entries are floating in these days.

The newest one is by Angeliki Koutsoukou-Argyraki and Wenda Li on
"Irrationality Criteria for Series by Erdős and Straus"


We formalise certain irrationality criteria for infinite series of the form:

    Sum_{n=1}^∞  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.
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.



See https://www.isa-afp.org/entries/Irrational_Series_Erdos_Straus.html for
more details.

Enjoy,
René

Attachment: signature.asc
Description: Message signed with OpenPGP



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.