Real helper lemmas for interval corner bounds

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

If $x\in[a,b]$ and $y\in[c,d]$, then $xy$ is enclosed by the minimum and maximum of the four corner products $\{ac,ad,bc,bd\}$.

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

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

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

def TorchLean.Floats.Interval.maxOfFourReal (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) : minOfFourReal (a * c) (a * d) (b * c) (b * d) ≤ x * y ∧ x * y ≤ maxOfFourReal (a * c) (a * d) (b * c) (b * d)

Corner enclosure for real 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 minOfFourReal/maxOfFourReal with the same grouping used by the IEEE32Exec 4-corner rule implementations.

theorem TorchLean.Floats.Interval.inv_mem_Icc (c d y : ℝ) (hy : y ∈ Set.Icc c d) (h0 : d < 0 ∨ 0 < c) : y⁻¹ ∈ Set.Icc d⁻¹ c⁻¹

Reciprocal enclosure for an interval that lies strictly on one side of zero.

If y ∈ [c, d] and either d < 0 or 0 < c, then inversion reverses the endpoints: y⁻¹ ∈ [d⁻¹, c⁻¹].

theorem TorchLean.Floats.Interval.div_bounds_Icc (a b c d x y : ℝ) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) (h0 : d < 0 ∨ 0 < c) : minOfFourReal (a / c) (a / d) (b / c) (b / d) ≤ x / y ∧ x / y ≤ maxOfFourReal (a / c) (a / d) (b / c) (b / d)

Four-corner enclosure for division by a sign-stable interval.

The denominator hypothesis excludes zero. The result follows by enclosing y⁻¹ with inv_mem_Icc and applying mul_bounds_Icc to x * y⁻¹.