Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/6553
Pełny rekord metadanych
Pole DC | Wartość | Język |
---|---|---|
dc.contributor.author | Watase, Yasushige | - |
dc.date.accessioned | 2018-05-11T07:20:21Z | - |
dc.date.available | 2018-05-11T07:20:21Z | - |
dc.date.issued | 2017 | - |
dc.identifier.citation | Formalized Mathematics, Volume 25, Issue 4, Pages 283–288 | - |
dc.identifier.issn | 1426-2630 | - |
dc.identifier.uri | http://hdl.handle.net/11320/6553 | - |
dc.description.abstract | 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. | - |
dc.language.iso | en | - |
dc.publisher | DeGruyter Open | - |
dc.subject | Diophantine approximation | - |
dc.subject | rational approximation | - |
dc.subject | Dirichlet | - |
dc.subject | Hurwitz | - |
dc.subject | Minkowski | - |
dc.title | Introduction to Diophantine Approximation. Part II | - |
dc.type | Article | - |
dc.identifier.doi | 10.1515/forma-2017-0027 | - |
dc.description.Affiliation | Suginami-ku Matsunoki 3-21-6 Tokyo, Japan | - |
dc.description.references | Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007/978-3-319-20615-8 17. | - |
dc.description.references | 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. | - |
dc.description.references | G.H. Hardy and E.M. Wright. An Introduction to the Theory of Numbers. Oxford University Press, 6th edition, 2008. | - |
dc.description.references | Adolf Hurwitz. Ueber die angenäherte Darstellung der Irrationalzahlen durch rationale Brüche. Mathematische Annalen, 39(2):279-284, B.G.Teubner Verlag, Leipzig, 1891. | - |
dc.description.references | Hermann Minkowski. Diophantische Approximationen: eine Einf¨uhrung in die Zahlentheorie. Teubner, Leipzig, 1907. | - |
dc.description.references | Ivan Niven. Diophantine Approximation. Dover, 2008. | - |
dc.description.references | Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825-829, 2001. | - |
dc.description.references | Yasushige Watase. Introduction to Diophantine approximation. Formalized Mathematics, 23(2):101-106, 2015. doi: 10.1515/forma-2015-0010. | - |
dc.identifier.eissn | 1898-9934 | - |
dc.description.volume | 25 | - |
dc.description.issue | 4 | - |
dc.description.firstpage | 283 | - |
dc.description.lastpage | 288 | - |
dc.identifier.citation2 | Formalized Mathematics | - |
Występuje w kolekcji(ach): | Formalized Mathematics, 2017, Volume 25, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2017-0027.pdf | 296,02 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL