Show that floating point √x⋅x≥x\sqrt{x \cdot x} \geq x for all long xx.

I verified experimentally that in Java the equality

Math.sqrt(x*x) = x

holds for all long x such that x*x doesn’t overflow. Here, Java long is a 64 bit signed type and double is a IEEE binary floating point type with at least 53 bits mantissa and sufficiently long exponent.

Mathematically, there are two imprecise functions involved:

  • Conversion from long to double which loses precision due to the mantissa being only 53 bits where 63 bits would be needed. This operation is guaranteed to return the closest representable result.
  • Computing square root, which is also guaranteed to return the closest representable result.

Mathematically, this can be expressed like


where round is the rounding function from R into the set of all numbers representable as double.

I’m looking for a proof since no experiment can assure it works across all machines.


The idea is simple: Find upper and lower bounds for


and show that round(X)=x.

Let ulp(x) denote the unit of least precision at x
and let E(x) and M(x) denote the exponent and mantissa of x, i.e.,


with 1M(x)<2 and E(x)Z. Define


where μ=252 is the machine epsilon.

Expressing the rounding function by its relative error leads to


We know that |ϵ|12Δ(x2) and get (ignoring the trivial case x=0)


By observing M(x) and M(x2) e.g. over the interval [1,4],
it can be easily be shown that M(x)M(x2)2 which gives us


and therefore


Analogously we get the corresponding lower bound. Just instead of


we use something like


which suffices, since we used a very generous estimate (2/4<12) in the last step.

Because of |Xx| being smaller than 12ulp(x), x is the double closest to X, therefore round(X) must equal to x, q.e.d.

Source : Link , Question Author : maaartinus , Answer Author : maaartinus

Leave a Comment