# Volume 25 (2017): Issue 1 (March 2017)

Journal Details
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

7 Articles
Open Access

#### Fubini’s Theorem on Measure

Published Online: 11 May 2017
Page range: 1 - 29

#### Abstract

The purpose of this article is to show Fubini’s theorem on measure [16], [4], [7], [15], [18]. Some theorems have the possibility of slight generalization, but we have priority to avoid the complexity of the description. First of all, for the product measure constructed in [14], we show some theorems. Then we introduce the section which plays an important role in Fubini’s theorem, and prove the relevant proposition. Finally we show Fubini’s theorem on measure.

#### Keywords

• Fubini’s theorem
• product measure

• 28A35
• 03B35

#### MML

• identifier: MEASUR11
• version: 8.1.05 5.40.1286
Open Access

#### Differentiability of Polynomials over Reals

Published Online: 11 May 2017
Page range: 31 - 37

#### Abstract

In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].

#### Keywords

• differentiation of real polynomials
• derivative of real polynomials

• 26A24
• 03B35

#### MML

• identifier: POLYDIFF
• version: 8.1.05 5.40.1286
Open Access

#### Introduction to Liouville Numbers

Published Online: 11 May 2017
Page range: 39 - 48

#### Abstract

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

• Liouville number
• Diophantine approximation
• transcendental number
• Liouville constant

• 11J81
• 11K60
• 03B35

#### MML

• identifier: LIOUVIL1
• version: 8.1.05 5.40.1286
Open Access

#### All Liouville Numbers are Transcendental

Published Online: 11 May 2017
Page range: 49 - 54

#### Abstract

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

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.

#### Keywords

• Liouville number
• Diophantine approximation
• transcendental number
• Liouville constant

• 11J81
• 11K60
• 03B35

#### MML

• identifier: LIOUVIL1
• version: 8.1.05 5.40.1286
Open Access

#### Group of Homography in Real Projective Plane

Published Online: 11 May 2017
Page range: 55 - 62

#### Abstract

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.

Then, we prove that, using the notations of Borsuk and Szmielew in [3]

“Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.”

(Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11]

“Let [a], [b], [c], [d] in ℝℙ2 be four points of which no three are collinear and let [a′],[b′],[c′],[d′] in ℝℙ2 be another four points of which no three are collinear, then there exists a 3 × 3 matrix M such that [Ma] = [a′], [Mb] = [b′], [Mc] = [c′], and [Md] = [d′]”

Makarios has formalized the same results in Isabelle/Isar (the collineations form a group, lemma statement52-existence and lemma statement 53-existence) and published it in Archive of Formal Proofs [10], [9].

#### Keywords

• projectivity
• projective transformation
• real projective plane
• group of homography

• 51N15
• 03B35

#### MML

• identifier: ANPROJ_9
• version: 8.1.05 5.40.1289
Open Access

#### Ordered Rings and Fields

Published Online: 11 May 2017
Page range: 63 - 72

#### Abstract

We introduce ordered rings and fields following Artin-Schreier’s approach using positive cones. We show that such orderings coincide with total order relations and give examples of ordered (and non ordered) rings and fields. In particular we show that polynomial rings can be ordered in (at least) two different ways [8, 5, 4, 9]. This is the continuation of the development of algebraic hierarchy in Mizar [2, 3].

#### Keywords

• commutative algebra
• ordered fields
• positive cones

• 12J15
• 03B35

#### MML

• identifier: REALALG1
• version: 8.1.05 5.40.1289
Open Access

#### Embedded Lattice and Properties of Gram Matrix

Published Online: 11 May 2017
Page range: 73 - 86

#### Abstract

In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].

#### Keywords

• Z-lattice
• Gram matrix
• rational Z-lattice

• 15A09
• 15A63
• 03B35

#### MML

• identifier: ZMODLAT2
• version: 8.1.05 5.40.1289