<abstract xmlns="http://www.w3.org/1999/xhtml"> 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. </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.

Introduction to Diophantine Approximation. Part II

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

{"article-title":"Introduction to Diophantine Approximation. Part II"}

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

Introduction to Diophantine Approximation. Part II

Published Online: Mar 28, 2018

Page range: 283 - 288

Received: Nov 29, 2017

DOI: https://doi.org/10.1515/forma-2017-0027

Keywords
Diophantine approximation, rational approximation, Dirichlet, Hurwitz, Minkowski

© by Yasushige Watase

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Introduction to Diophantine Approximation. Part II

Published Online: Mar 28, 2018

Page range: 283 - 288

Received: Nov 29, 2017

DOI: https://doi.org/10.1515/forma-2017-0027

KeywordsDiophantine approximation, rational approximation, Dirichlet, Hurwitz, Minkowski

© by Yasushige Watase

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Keywords
Diophantine approximation, rational approximation, Dirichlet, Hurwitz, Minkowski