The Transcendence of Certain Infinite Series

Title:	The Transcendence of Certain Infinite Series
Authors:	Angeliki Koutsoukou-Argyraki and Wenda Li
Submission date:	2019-03-27
Abstract:	We formalize the proofs of two transcendence criteria by J. Hančl and P. Rucki that assert the transcendence of the sums of certain infinite series built up by sequences that fulfil certain properties. Both proofs make use of Roth's celebrated theorem on diophantine approximations to algebraic numbers from 1955 which we implement as an assumption without having formalised its proof.
BibTeX:	@article{Transcendence_Series_Hancl_Rucki-AFP, author = {Angeliki Koutsoukou-Argyraki and Wenda Li}, title = {The Transcendence of Certain Infinite Series}, journal = {Archive of Formal Proofs}, month = mar, year = 2019, note = {\url{http://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Prime_Number_Theorem
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.