REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/5567
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorGrabowski, Adam-
dc.contributor.authorKorniłowicz, Artur-
dc.date.accessioned2017-06-05T08:32:50Z-
dc.date.available2017-06-05T08:32:50Z-
dc.date.issued2017-
dc.identifier.citationFormalized Mathematics, Volume 25, Issue 1, pp. 39-48pl
dc.identifier.issn1426-2630pl
dc.identifier.issn1898-9934pl
dc.identifier.urihttp://hdl.handle.net/11320/5567-
dc.description.abstractThe article defines Liouville numbers, originally introduced by Joseph Liouville in 1844 [17] 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. Liouville constant, which is also defined formally, is the first transcendental (not algebraic) number. It is defined in Section 6 quite generally as the sum X∞ k=1 ak b k! for a finite sequence {ak}k∈N and b ∈ N. Based on this definition, we also introduced the so-called Liouville number as L = X∞ k=1 10−k! = 0.110001000000000000000001 . . . , substituting in the definition of L(ak, b) the constant sequence of 1’s and b = 10. Another important examples of transcendental numbers are e and π [7], [13], [6]. At the end, we show that the construction of an arbitrary Lioville constant satisfies the properties of a Liouville number [12], [1]. We show additionally, that the set of all Liouville numbers is infinite, opening the next item from Abad and Abad’s list of “Top 100 Theorems”. We show also some preliminary constructions linking real sequences and finite sequences, where summing formulas are involved. In the Mizar [14] proof, we follow closely https: //en.wikipedia.org/wiki/Liouville_number. The aim is to show that all Liouville numbers are transcendental.-
dc.language.isoen-
dc.publisherDe Gruyter Open-
dc.subjectLiouville number-
dc.subjectDiophantine approximation-
dc.subjecttranscendental number-
dc.subjectLiouville constant-
dc.titleIntroduction to Liouville Numbers-
dc.typeArticle-
dc.identifier.doi10.1515/forma-2017-0003-
dc.description.AffiliationGrabowski Adam - Institute of Informatics, University of Białystok, Białystok, Poland-
dc.description.AffiliationKorniłowicz Artur - Institute of Informatics, University of Białystok, Białystok, Poland-
dc.description.referencesTom M. Apostol. Modular Functions and Dirichlet Series in Number Theory. Springer- Verlag, 2nd edition, 1997.-
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.-
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.-
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.-
dc.description.referencesGrzegorz Bancerek and Piotr Rudnicki. Two programs for SCM. Part I - preliminaries. Formalized Mathematics, 4(1):69-72, 1993.-
dc.description.referencesSophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials. In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 76-87. ACM, 2016.-
dc.description.referencesJesse Bingham. Formalizing a proof that e is transcendental. Journal of Formalized Reasoning, 4:71-84, 2011.-
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.-
dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.-
dc.description.referencesCzesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521-527, 1990.-
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.-
dc.description.referencesJ.H. Conway and R.K. Guy. The Book of Numbers. Springer-Verlag, 1996.-
dc.description.referencesManuel Eberl. Liouville numbers. Archive of Formal Proofs, December 2015. http://isa-afp.org/entries/Liouville_Numbers.shtml, Formal proof development.-
dc.description.referencesAdam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015.-
dc.description.referencesJarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.-
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.-
dc.description.referencesJoseph Liouville. Nouvelle démonstration d’un théorème sur les irrationnelles algébriques, inséré dans le Compte Rendu de la dernière séance. Compte Rendu Acad. Sci. Paris, Sér.A (18):910–911, 1844.-
dc.description.referencesJan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990.-
dc.description.referencesKonrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125-130, 1991.-
dc.description.referencesKonrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216, 1991.-
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.-
dc.description.referencesWojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.-
dc.description.referencesWojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1 (5):979-981, 1990.-
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.-
Występuje w kolekcji(ach):Artykuły naukowe (WInf)
Formalized Mathematics, 2017, Volume 25, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2017-0003.pdf292,86 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


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