Outward-rounded arithmetic for Model.Interval

Each endpoint operation uses the corresponding directed Model kernel. Multiplication and division use the classical four-corner construction. Division returns the whole interval when the denominator contains zero, covering quotient sets that may be disconnected or unbounded. Addition, subtraction, multiplication, and division pass computed endpoints through ofBounds, replacing NaN or reversed endpoints with the format's whole range. For formats without infinity, enclosing real results needs the relevant range bounds.

The finite endpoint formulas and outward rounding are described in Rump's Verification methods, §§5.1 and 5.3.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add {fmt : FloatFormat} (A B : Interval fmt) : Interval fmt

Outward-rounded interval addition.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.neg {fmt : FloatFormat} (A : Interval fmt) : Interval fmt

Interval negation, reversing and negating the endpoints.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub {fmt : FloatFormat} (A B : Interval fmt) : Interval fmt

Outward-rounded interval subtraction.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul {fmt : FloatFormat} (A B : Interval fmt) : Interval fmt

Outward-rounded interval multiplication using all four endpoint products.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.div {fmt : FloatFormat} (A B : Interval fmt) : Interval fmt

Outward-rounded interval division.

When the denominator contains zero, the result is whole fmt. Otherwise all four directed quotients determine the endpoint enclosure.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.inv {fmt : FloatFormat} (B : Interval fmt) : Interval fmt

Interval reciprocal, conservatively returning whole fmt when zero is included.