Distance to the nearest integer (source code)

= Distance to the nearest integer
{title2=$\|x\|_{\mathbb R/\mathbb Z}$}

= Distance modulo one
{synonym}

For a <real number> $x$, define $\|x\|_{\mathbb R/\mathbb Z}=\min_{k\in\mathbb Z}|x-k|$. It lies in $[0,1/2]$ and obeys $\|\ell x\|\leq|\ell|\|x\|$ for an <integer> $\ell$. It is a distance on the circle, rather than a <norm> on the real vector space.