REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/6553`
 Tytuł: Introduction to Diophantine Approximation. Part II Autorzy: Watase, Yasushige Słowa kluczowe: Diophantine approximationrational approximationDirichletHurwitzMinkowski Data wydania: 2017 Data dodania: 11-maj-2018 Wydawca: DeGruyter Open Źródło: Formalized Mathematics, Volume 25, Issue 4, Pages 283–288 Abstrakt: In the article we present in the Mizar system [1], [2] the formalized proofs for Hurwitz’ theorem [4, 1891] and Minkowski’s theorem [5]. Both theorems are well explained as a basic result of the theory of Diophantine approximations appeared in [3], [6]. A formal proof of Dirichlet’s theorem, namely an inequation |θ−y/x| ≤ 1/x2 has infinitely many integer solutions (x, y) where θ is an irrational number, was given in [8]. A finer approximation is given by Hurwitz’ theorem: |θ− y/x|≤ 1/√5x2. Minkowski’s theorem concerns an inequation of a product of non-homogeneous binary linear forms such that |a1x + b1y + c1| · |a2x + b2y + c2| ≤ ∆/4 where ∆ = |a1b2 − a2b1| ≠ 0, has at least one integer solution. Afiliacja: Suginami-ku Matsunoki 3-21-6 Tokyo, Japan URI: http://hdl.handle.net/11320/6553 DOI: 10.1515/forma-2017-0027 ISSN: 1426-2630 e-ISSN: 1898-9934 Typ Dokumentu: Article Występuje w kolekcji(ach): Formalized Mathematics, 2017, Volume 25, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat