Sterbenz's Lemma for Gradual Underflow

Sterbenz exact subtraction extends from the unbounded-exponent family FLX to the gradual-underflow family FLT. The latter is the format used by the rounded-real binary32 model.

The proof splits on the magnitude of the exact difference. Every FLT operand lies on the minimum-exponent grid, so a sufficiently small difference is representable by closure of that grid under subtraction. A larger difference follows from the FLX Sterbenz theorem and the normal-range inclusion from FLX to FLT.

Reference

• P. H. Sterbenz, Floating-Point Computation, Prentice-Hall, 1974.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLX_to_FLT_of_normal {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hxFLX : genericFormat β (flxExp prec) x) (hnorm : bpow β (emin + prec - 1) ≤ |x|) : genericFormat β (fltExp emin prec) x

An FLX value in the normal range is representable in the corresponding FLT format.

This is the normal-range converse of generic_format_FLT_to_FLX.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLT_sub_of_le_two_mul {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hy : 0 < y) (hyx : y ≤ x) (hx2y : x ≤ 2 * y) (hxFmt : genericFormat β (fltExp emin prec) x) (hyFmt : genericFormat β (fltExp emin prec) y) : genericFormat β (fltExp emin prec) (x - y)

Directed Sterbenz lemma for FLT: if 0 < y ≤ x ≤ 2y and both operands are representable, then their exact difference is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLT_sterbenz {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hx2y : x ≤ 2 * y) (hy2x : y ≤ 2 * x) (hxFmt : genericFormat β (fltExp emin prec) x) (hyFmt : genericFormat β (fltExp emin prec) y) : genericFormat β (fltExp emin prec) (x - y)

Sterbenz's lemma for FLT: if two positive representable values are within a factor of two, then their exact difference is representable, including across the subnormal boundary.