<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

Published Online: Aug 13, 2015

Page range: 101 - 106

Received: Apr 19, 2015

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

Keywords
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

Published Online: Aug 13, 2015

Page range: 101 - 106

Received: Apr 19, 2015

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

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

Keywords
irrational number, approximation, continued fraction, rational number, Dirichlet’s proof