Range-limited finite-only interval enclosures #
Finite-only formats saturate instead of producing infinity, so their outward interval operations are sound only when the exact endpoint expressions stay inside the finite range. The theorems here state those range premises.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add_sound_of_encoding_finite
{fmt : FloatFormat}
(A B : Interval fmt)
(hfmt : fmt.encoding = FloatFormat.Encoding.finite)
(hloRange : |A.lo.toReal + B.lo.toReal| ≤ (posMaxFinite fmt).toReal)
(hhiRange : |A.hi.toReal + B.hi.toReal| ≤ (posMaxFinite fmt).toReal)
{x y : ℝ}
(hx : A.RealMem x)
(hy : B.RealMem y)
:
Finite-only interval addition encloses every selected sum when both exact endpoint sums fit in the format's symmetric finite range.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub_sound_of_encoding_finite
{fmt : FloatFormat}
(A B : Interval fmt)
(hfmt : fmt.encoding = FloatFormat.Encoding.finite)
(hloRange : |A.lo.toReal - B.hi.toReal| ≤ (posMaxFinite fmt).toReal)
(hhiRange : |A.hi.toReal - B.lo.toReal| ≤ (posMaxFinite fmt).toReal)
{x y : ℝ}
(hx : A.RealMem x)
(hy : B.RealMem y)
:
Finite-only interval subtraction is sound when its two exact endpoint differences fit in range.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul_sound_of_encoding_finite
{fmt : FloatFormat}
(A B : Interval fmt)
(hfmt : fmt.encoding = FloatFormat.Encoding.finite)
(h00 : |A.lo.toReal * B.lo.toReal| ≤ (posMaxFinite fmt).toReal)
(h01 : |A.lo.toReal * B.hi.toReal| ≤ (posMaxFinite fmt).toReal)
(h10 : |A.hi.toReal * B.lo.toReal| ≤ (posMaxFinite fmt).toReal)
(h11 : |A.hi.toReal * B.hi.toReal| ≤ (posMaxFinite fmt).toReal)
{x y : ℝ}
(hx : A.RealMem x)
(hy : B.RealMem y)
:
Finite-only interval multiplication is sound when all four exact corner products fit in range.