Sterbenz lemma

In floating-point arithmetic, the Sterbenz lemma or Sterbenz' lemma is a theorem giving conditions under which floating-point differences are computed exactly. It is named after Pat H. Sterbenz, who published it as Theorem 4.3.1 in his 1974 book "Floating-Point Computation".
The Sterbenz lemma states that for a floating-point number system with subnormal numbers, such as IEEE 754 binary64, if formula_1 and formula_2 are floating-point numbers such that
formula_3
then formula_4 is also a floating-point number.
Thus, the floating-point subtraction formula_5 is computed exactly.
Relation to catastrophic cancellation.
The Sterbenz lemma may be contrasted with the phenomenon of catastrophic cancellation:
In other words, the Sterbenz lemma shows that subtracting nearby floating-point numbers is exact, but if the numbers you have are approximations then even their exact difference may be far off from the difference of numbers you wanted to subtract.
Use in numerical analysis.
The Sterbenz lemma is instrumental in proving theorems on error bounds in numerical analysis of floating-point algorithms.
For example, Heron's formula
formula_21
for the area of triangle with side lengths formula_22, formula_23, and formula_24, where formula_25 is the semi-perimeter, may give poor accuracy for long narrow triangles if evaluated directly in floating-point arithmetic.
However, the alternative formula
formula_26
can be proven, with the help of the Sterbenz lemma, to have low forward error for all inputs.