Containment for interval multiply-add

Four-corner product bounds followed by the addend bounds enclose every real combination of the inputs. Rounding takes place after this exact calculation.

theorem FloatLib.Numerics.Interval.fma_bounds {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (I J K : Interval β) {x y z : β} (hx : I.lo ≤ x ∧ x ≤ I.hi) (hy : J.lo ≤ y ∧ y ≤ J.hi) (hz : K.lo ≤ z ∧ z ≤ K.hi) : (I.fmaBounds J K).lo ≤ x * y + z ∧ x * y + z ≤ (I.fmaBounds J K).hi

Exact multiply-add bounds contain every combination of members of the three intervals.

theorem FloatLib.Numerics.Interval.contains_fma? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I J K L : Interval α} (h : fma? R I J K = some L) {x y z : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) (hz : Contains R.decode K z) : Contains R.decode L (x * y + z)

Any outward rounder preserves the exact multiply-add bounds over its ordered field.

theorem FloatLib.Numerics.Interval.containsReal_fma? {α : Type u_1} (R : OutwardRounding α ℚ) {I J K L : Interval α} (h : fma? R I J K = some L) {x y z : ℝ} (hx : ContainsReal R.decode I x) (hy : ContainsReal R.decode J y) (hz : ContainsReal R.decode K z) : ContainsReal R.decode L (x * y + z)

Successful multiply-add encloses arbitrary real members of rationally decoded intervals.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_fma (precision : ℕ) {I J K : Interval ℤ} {x y z : ℝ} (hx : ContainsReal (decode precision) I x) (hy : ContainsReal (decode precision) J y) (hz : ContainsReal (decode precision) K z) : ContainsReal (decode precision) (fma precision I J K) (x * y + z)

Integer multiply-add contains the exact real expression before its final outward rounding.