1. bookVolume 25 (2017): Issue 1 (March 2017)
Journal Details
License
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English
access type Open Access

Introduction to Liouville Numbers

Published Online: 11 May 2017
Volume & Issue: Volume 25 (2017) - Issue 1 (March 2017)
Page range: 39 - 48
Received: 23 Feb 2017
Journal Details
License
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English
Summary

The 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

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

for a finite sequence {ak}k∈ℕ and b ∈ ℕ. Based on this definition, we also introduced the so-called Liouville number as

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.

Keywords

MSC

MML

[1] Tom M. Apostol. Modular Functions and Dirichlet Series in Number Theory. Springer- Verlag, 2nd edition, 1997.Search in Google Scholar

[2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.Search in Google Scholar

[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.Search in Google Scholar

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.Search in Google Scholar

[5] Grzegorz Bancerek and Piotr Rudnicki. Two programs for SCM. Part I - preliminaries. Formalized Mathematics, 4(1):69-72, 1993.Search in Google Scholar

[6] Sophie 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. doi: 10.1145/2854065.2854072.10.1145/2854065.2854072Search in Google Scholar

[7] Jesse Bingham. Formalizing a proof that e is transcendental. Journal of Formalized Reasoning, 4:71-84, 2011.Search in Google Scholar

[8] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.Search in Google Scholar

[9] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.Search in Google Scholar

[10] Czesł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.Search in Google Scholar

[11] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.Search in Google Scholar

[12] J.H. Conway and R.K. Guy. The Book of Numbers. Springer-Verlag, 1996.10.1007/978-1-4612-4072-3Search in Google Scholar

[13] Manuel Eberl. Liouville numbers. Archive of Formal Proofs, December 2015. http://isa-afp.org/entries/Liouville_Numbers.shtml, Formal proof development.Search in Google Scholar

[14] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1Search in Google Scholar

[15] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.Search in Google Scholar

[16] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.Search in Google Scholar

[17] Joseph Liouville. Nouvelle d´emonstration d’un th´eor`eme sur les irrationnelles alg´ebriques, ins´er´e dans le Compte Rendu de la derni`ere s´eance. Compte Rendu Acad. Sci. Paris, S´er.A (18):910-911, 1844.Search in Google Scholar

[18] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990.Search in Google Scholar

[19] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125-130, 1991.Search in Google Scholar

[20] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216, 1991.Search in Google Scholar

[21] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.Search in Google Scholar

[22] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.Search in Google Scholar

[23] Wojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1 (5):979-981, 1990.Search in Google Scholar

[24] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.Search in Google Scholar

Recommended articles from Trend MD

Plan your remote conference with Sciendo