Ordered-field interval corner bounds

Multiplication and division away from zero are enclosed by their four endpoint calculations. The proofs apply to any ordered field, independently of endpoint representation or rounding.

The corner rule is equation (5.4) in S. M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §5.1.

@[reducible, inline]

abbrev FloatLib.Numerics.Interval.minOfFour {α : Type u_2} [LinearOrder α] (a b c d : α) : α

Minimum of four ordered values, grouped as min (min a b) (min c d).

@[reducible, inline]

abbrev FloatLib.Numerics.Interval.maxOfFour {α : Type u_2} [LinearOrder α] (a b c d : α) : α

Maximum of four ordered values, grouped as max (max a b) (max c d).

theorem FloatLib.Numerics.Interval.mul_bounds_Icc {β : Type u_1} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (a b c d x y : β) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) : x * y ∈ Set.Icc (minOfFour (a * c) (a * d) (b * c) (b * d)) (maxOfFour (a * c) (a * d) (b * c) (b * d))

Corner enclosure for multiplication on intervals.

If $x\in[a,b]$ and $y\in[c,d]$, then $$ \min(ac,ad,bc,bd)\le xy\le\max(ac,ad,bc,bd), $$

where the min/max are represented by minOfFour/maxOfFour with the same grouping used by the executable interval four-corner rule.

theorem FloatLib.Numerics.Interval.div_bounds_Icc {β : Type u_1} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (a b c d x y : β) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) (hzero : d < 0 ∨ 0 < c) : x / y ∈ Set.Icc (minOfFour (a / c) (a / d) (b / c) (b / d)) (maxOfFour (a / c) (a / d) (b / c) (b / d))

Corner enclosure for division when the denominator interval lies strictly on one side of zero.