REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/5568
Tytuł: All Liouville Numbers are Transcendental
Autorzy: Korniłowicz, Artur
Naumowicz, Adam
Grabowski, Adam
Słowa kluczowe: Liouville number
Diophantine approximation
transcendental number
Liouville constant
Data wydania: 2017
Data dodania: 5-cze-2017
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 25, Issue 1, pp. 49-54
Abstrakt: In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and 0 < x − p q < 1 q n . It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in [10], [1], and [12]. Liouvile constant, which is defined formally in [12], is the first explicit transcendental (not algebraic) number, another notable examples are e and π [5], [11], and [4]. Algebraic numbers were formalized with the help of the Mizar system [13] very recently, by Yasushige Watase in [23] and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.
Afiliacja: Korniłowicz Artur - Institute of Informatics, University of Białystok, Białystok, Poland
Naumowicz Adam - Institute of Informatics, University of Białystok, Białystok, Poland
Grabowski Adam - Institute of Informatics, University of Białystok, Białystok, Poland
URI: http://hdl.handle.net/11320/5568
DOI: 10.1515/forma-2017-0004
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2017, Volume 25, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2017-0004.pdf264,56 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons