<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

Publicado en línea: 13 ago 2015

Páginas: 101 - 106

Recibido: 19 abr 2015

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

Palabras clave
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

Publicado en línea: 13 ago 2015

Páginas: 101 - 106

Recibido: 19 abr 2015

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

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

Palabras clave
irrational number, approximation, continued fraction, rational number, Dirichlet’s proof