Sterbenz lemma

In floating-point arithmetic, the Sterbenz lemma or Sterbenz's lemma is a theorem giving conditions under which floating-point differences are computed exactly. It is named after Pat H. Sterbenz, who published a variant of it in 1974.

Sterbenz lemma—In a floating-point number system with subnormal numbers, if $x$ and $y$ are floating-point numbers such that

${\frac {y}{2}}\leq x\leq 2y,$

then $x-y$ is also a floating-point number. Thus, a correctly rounded floating-point subtraction

$x\ominus y=\operatorname {fl} (x-y)=x-y$

is computed exactly.

The Sterbenz lemma applies to IEEE 754, the most widely used floating-point number system in computers.