Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Irrationality Criteria for Ser...


view this post on Zulip Email Gateway (Aug 23 2022 at 09:08):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
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é
signature.asc


Last updated: Apr 26 2024 at 08:19 UTC