A refinement of a given reciprocal approximation may be derived in two steps:
PROOF: Let and . Then , , and
The inequality (b) of Lemma 13.2.1 provides a significantly reduced error bound for a refined reciprocal approximation as long as the bounds and for the earlier approximations and are large in comparison to . To establish the bound for the final approximation as required by Lemma 13.1.2, we shall use the inequality (a), pertaining to the corresponding unrounded value, in conjunction with the following additional lemma, which is a variation by Harrison [HAR00] of another result of Markstein [MAR90]. In practice, the application of this lemma involves explicitly checking a small number of excluded cases.
PROOF: If , then implies and . Thus we may assume , and therefore . Consequently,
David Russinoff 2017-08-01