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.

@[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.