>>253
一般に、xを代数的無理数と仮定すると、ロスの定理により、
任意の ε>0 に対して、高々有限個の有理数 q/p (p,q)=1 p≧1 が存在して
|x−(q/p)|<1/p^{2+ε} が成り立つ
という書き方だと、xやεの取り方によっては
|x−(q/p)|<1/p^{2+ε} なる有理数 q/p (p,q)=1 p≧1 が
存在することもあれば存在しないこともあるから、
任意の代数的無理数x、任意の ε>0 に対して、或る正の実数 C(x,ε) が存在して
無限個の有理数 q/p (p,q)=1 p≧1 に対して
1/p^2>|x−(q/p)|>C(x,ε)/p^{2+ε} が成立し、p^ε>C(x,ε) である
また、最小値の原理より、1/p^2>|x−(q/p)|>C(x,ε)/p^{2+ε} なる
有理数 q/p (p,q)=1 p≧1 の分母pの最小値 M(p) が存在する
よって、正の実数 C(x,ε) は、C(x,ε)<(M(p))^ε と上から評価出来る
正の実数 C(x,ε) は計算可能ではない