In this article we formalize some results of Diophantine approximation, i.e. the approximation of an irrational number by rationals. A typical example is finding an integer solution (x, y) of the inequality |xθ − y| ≤ 1/x, where 0 is a real number. First, we formalize some lemmas about continued fractions. Then we prove that the inequality has infinitely many solutions by continued fractions. Finally, we formalize Dirichlet’s proof (1842) of existence of the solution [12], [1].
This article provides a formalized proof of the so-called “the four-square theorem”, namely any natural number can be expressed by a sum of four squares, which was proved by Lagrange in 1770. An informal proof of the theorem can be found in the number theory literature, e.g. in [14], [1] or [23]. This theorem is item #19 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [14], [1], [10] and [7] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial...
This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).
This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called L1 space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions...
In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.
Download Results (CSV)