DOIAbstract
AbstractIn 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].Suginami-ku Matsunoki 6, 3-21 Tokyo, JapanAlan Baker. A Concise Introduction to the Theory of Numbers. Cambridge University Press, 1984.Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.Grzegorz Bancerek. The fundamental propertie...
Add to ORKG