Real helper lemmas for interval corner bounds

Several IEEEExec32 interval-soundness modules need the same basic real-analysis fact:

If x ∈ [a,b] and y ∈ [c,d], then x*y is enclosed by the minimum/maximum of the four corner products {a*c, a*d, b*c, b*d}.

This module keeps the interval arithmetic fact separate from the IEEEExec32 soundness proofs.

def TorchLean.Floats.Interval.min4R (a b c d : ℝ) : ℝ

Minimum of four real numbers, grouped as min (min a b) (min c d).

def TorchLean.Floats.Interval.max4R (a b c d : ℝ) : ℝ

Maximum of four real numbers, grouped as max (max a b) (max c d).

theorem TorchLean.Floats.Interval.mul_bounds_Icc (a b c d x y : ℝ) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) : min4R (a * c) (a * d) (b * c) (b * d) ≤ x * y ∧ x * y ≤ max4R (a * c) (a * d) (b * c) (b * d)

Corner enclosure for real multiplication on intervals.

If x ∈ [a,b] and y ∈ [c,d], then:

min(ac, ad, bc, bd) ≤ x*y ≤ max(ac, ad, bc, bd),

where the min/max are represented by min4R/max4R with the same grouping used by the IEEE32Exec 4-corner rule implementations.