Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

6 Formalized Mathematics

Znaleziono wyników: 6

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Lagrange’s Four-Square Theorem

100%

Watase Y.

Formalized Mathematics

2014

tom 22

nr 2

105-110

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/.

Introduction to Diophantine Approximation

100%

Watase Y.

Formalized Mathematics

2015

tom 23

nr 2

101-106

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].

Algebraic Numbers

100%

Watase Y.

Formalized Mathematics

2016

tom 24

nr 4

291-299

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 ring of ℚ[x] turns to be a field.

OnL1Space Formed by Real-Valued Partial Functions

51%

Watase Y. , Endou N. , Shidama Y.

Formalized Mathematics

2008

tom 16

nr 4

361-369

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 does not form an additive group due to lack of right zeroed condition. Therefore, firstly we introduced a kind of a quasi-linear space, then, we introduced the definition of an equivalent relation of two functions which are almost everywhere equal (=a.e.), thirdly we formalized a linear space by taking the quotient of a quasi-linear space by the relation (=a.e.).MML identifier: LPSPACE1, version: 7.9.03 4.108.1028

On L1Space Formed by Complex-Valued Partial Functions

51%

Watase Y. , Endou N. , Shidama Y.

Formalized Mathematics

2012

tom 20

nr 4

349-357

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.

On L p Space Formed by Real-Valued Partial Functions

51%

Watase Y. , Endou N. , Shidama Y.

Formalized Mathematics

2010

tom 18

nr 3

159-169

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]).