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

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

Introduction to Diophantine Approximation

Suginami-ku Matsunoki 6 3-21 Tokyo, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Introduction to Diophantine Approximation"}

In this article we formalize some results of Diophantine approximation, i.e. the approximation of an irrational number by rationals. A typical example is...

Introduction to Diophantine Approximation

Publié en ligne: 13 août 2015

Pages: 101 - 106

Reçu: 19 avr. 2015

DOI: https://doi.org/10.1515/forma-2015-0010

Mots clés
irrational number, approximation, continued fraction, rational number, Dirichlet’s proof

© by Yasushige Watase

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Introduction to Diophantine Approximation

Publié en ligne: 13 août 2015

Pages: 101 - 106

Reçu: 19 avr. 2015

DOI: https://doi.org/10.1515/forma-2015-0010

Mots clésirrational number, approximation, continued fraction, rational number, Dirichlet’s proof

© by Yasushige Watase

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Mots clés
irrational number, approximation, continued fraction, rational number, Dirichlet’s proof