Diophantine bound for the square root of two (source code)

= Diophantine bound for the square root of two
{c}
{title2=$\|q\sqrt2\|\geq1/(4q)$}

For the nearest integer $a$ to $q\sqrt2$, the nonzero integer $2q^2-a^2$ has absolute value at least one. Dividing by $q\sqrt2+a\leq4q$ proves the bound. Thus the points $0,\sqrt2,\ldots,W\sqrt2$ modulo one are separated by at least $1/(4W)$. Ordering their distances from zero gives $\sum_{h\leq W}\|h\sqrt2\|^{-1}\ll W\log(2W)$.