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 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/x 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/ √ 5x . 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| 6 = 0, has at least one integer solution.