Introduction to Diophantine Approximation
Copyright policy )Introduction to Diophantine Approximation
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].
Dirichlet’s proof, Mechanization of proofs and logical operations, rational number, Dirichlet's proof, Continued fractions, Approximation to algebraic numbers, irrational number, approximation, 510, continued fraction
Dirichlet’s proof, Mechanization of proofs and logical operations, rational number, Dirichlet's proof, Continued fractions, Approximation to algebraic numbers, irrational number, approximation, 510, continued fraction
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).1 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!