Interval multiply-add with one outward rounding

The product bounds and the addend are combined before rounding either endpoint. A finite endpoint format can therefore enclose a small final result even when the intermediate product would exceed its range. These operations enclose the real expression x * y + z.

def FloatLib.Numerics.Interval.fmaBounds {β : Type u_2} [Field β] [LinearOrder β] (I J K : Interval β) : Interval β

Exact endpoint bounds for a product followed by addition.

def FloatLib.Numerics.Interval.fma? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I J K : Interval α) : Option (Interval α)

Enclose x * y + z, rounding only the final lower and upper bounds.

Decoding or final endpoint overflow returns none. No representable intermediate product is required.

def FloatLib.Numerics.Interval.BinaryGrid.fma (precision : ℕ) (I J K : Interval ℤ) : Interval ℤ

Integer multiply-add, aligning the addend before the two outward-rounded shifts.