Quantized interval arithmetic (rounding on $\mathbb{R}$, overflow-aware)

This file provides a sound enclosure layer for real computations where interval endpoints are snapped outward to a chosen representable grid (a Flocq-style $(\beta,\mathtt{fexp})$ format).

The main intended use is verification/bounding:

• You start from a real interval $x\in[\mathtt{lo},\mathtt{hi}]$.
• You propagate it through primitive operations and monotone nonlinearities.
• After each primitive, you quantize the endpoint outward via a Rounder (down/up).

Compared to an executable IEEE kernel:

• This is proof-friendly (everything lives in $\mathbb{R}$ or EReal and uses Flocq-style rounding).
• It is not a bit-level IEEE-754 model (no NaN payloads, signed zero rules, etc.).

Overflow-awareness:

• We use EReal (extended reals) to represent unbounded intervals arising from division by an interval that contains $0$.

References:

• IEEE 1788-2015 (interval arithmetic).
• Moore, Kearfott, Cloud, Introduction to Interval Analysis (2009).
• Rump (INTLAB) for outward rounding.

structure TorchLean.Floats.Interval.RInterval : Type

A closed real interval $[\mathtt{lo},\mathtt{hi}]$.

• lo : ℝ

  lo.

• hi : ℝ

  hi.

def TorchLean.Floats.Interval.RInterval.mem (I : RInterval) (x : ℝ) : Prop

Membership predicate: $x\in I$ means $I.\mathtt{lo}\le x\le I.\mathtt{hi}$.

@[implicit_reducible]

instance TorchLean.Floats.Interval.RInterval.instMembershipReal : Membership ℝ RInterval

Enable $x\in I$ notation for real intervals.

@[simp]

theorem TorchLean.Floats.Interval.RInterval.mem_iff (I : RInterval) (x : ℝ) : x ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi

Unfold membership: $x\in I\iff I.\mathtt{lo}\le x\land x\le I.\mathtt{hi}$.

def TorchLean.Floats.Interval.RInterval.Valid (I : RInterval) : Prop

Validity predicate: endpoints are ordered ($\mathtt{lo}\le\mathtt{hi}$).

@[inline]

def TorchLean.Floats.Interval.RInterval.point (x : ℝ) : RInterval

Degenerate interval $[x,x]$.

@[simp]

theorem TorchLean.Floats.Interval.RInterval.mem_point (x y : ℝ) : x ∈ point y ↔ x = y

Membership in a point interval is equality.

@[inline]

def TorchLean.Floats.Interval.RInterval.neg (I : RInterval) : RInterval

Interval negation: $-[\mathtt{lo},\mathtt{hi}]=[-\mathtt{hi},-\mathtt{lo}]$.

@[inline]

def TorchLean.Floats.Interval.RInterval.add (R : Rounder) (A B : RInterval) : RInterval

Outward-rounded interval addition, using the provided endpoint Rounder.

@[inline]

def TorchLean.Floats.Interval.RInterval.sub (R : Rounder) (A B : RInterval) : RInterval

Interval subtraction, implemented as $A+(-B)$ so soundness reuses mem_add and mem_neg.

noncomputable def TorchLean.Floats.Interval.RInterval.absMax (I : RInterval) : ℝ

Maximum absolute endpoint magnitude: $\max(|\mathtt{lo}|,|\mathtt{hi}|)$.

This is a convenient (and very proof-stable) way to get a coarse enclosure for products.

theorem TorchLean.Floats.Interval.RInterval.abs_le_absMax {I : RInterval} {x : ℝ} (hx : x ∈ I) : |x| ≤ I.absMax

If $x\in I$, then $|x|\le\operatorname{absMax}(I)$.

noncomputable def TorchLean.Floats.Interval.RInterval.mul (R : Rounder) (A B : RInterval) : RInterval

Loose-but-sound multiplication enclosure.

For $x\in A$ and $y\in B$, we have $|xy|\le\operatorname{absMax}(A)\operatorname{absMax}(B)$, hence $xy\in[-M,M]$. We then outward-round the endpoints via R.

This bound is conservative and serves as a generally applicable, proof-stable fallback. The executable IEEE interval layer provides the tighter four-corner multiplication theorem when that extra precision matters.

theorem TorchLean.Floats.Interval.RInterval.mem_add {R : Rounder} {A B : RInterval} {x y : ℝ} (hx : x ∈ A) (hy : y ∈ B) : x + y ∈ add R A B

Soundness of add: membership is preserved by real addition.

theorem TorchLean.Floats.Interval.RInterval.mem_sub {R : Rounder} {A B : RInterval} {x y : ℝ} (hx : x ∈ A) (hy : y ∈ B) : x - y ∈ sub R A B

Soundness of sub: membership is preserved by real subtraction.

theorem TorchLean.Floats.Interval.RInterval.mem_mul {R : Rounder} {A B : RInterval} {x y : ℝ} (hx : x ∈ A) (hy : y ∈ B) : x * y ∈ mul R A B

Soundness of the conservative mul enclosure: membership is preserved by real multiplication.

noncomputable def TorchLean.Floats.Interval.RInterval.exp (R : Rounder) (A : RInterval) : RInterval

Outward-rounded interval enclosure for Real.exp, using monotonicity.

theorem TorchLean.Floats.Interval.RInterval.mem_exp {R : Rounder} {A : RInterval} {x : ℝ} (hx : x ∈ A) : Real.exp x ∈ exp R A

Soundness of exp: membership is preserved by Real.exp.

noncomputable def TorchLean.Floats.Interval.RInterval.tanhBounds (R : Rounder) : RInterval

Coarse tanh enclosure $[-1,1]$ with outward-rounded endpoints.

We use this instead of a tighter monotone bound because tanh is bounded everywhere and the uniform bound is often enough for verification pipelines.

theorem TorchLean.Floats.Interval.RInterval.mem_tanhBounds {R : Rounder} (x : ℝ) : Real.tanh x ∈ tanhBounds R

Soundness of tanhBounds: $\tanh x\in[-1,1]$.

noncomputable def TorchLean.Floats.Interval.RInterval.tanh (R : Rounder) (_A : RInterval) : RInterval

Interval tanh enclosure.

This deliberately returns the global codomain enclosure tanhBounds. It is a proof-stable fallback for pipelines that only need a sound bound; monotone interval refinements can live beside it without changing this simple contract.

theorem TorchLean.Floats.Interval.RInterval.mem_tanh {R : Rounder} {A : RInterval} {x : ℝ} (_hx : x ∈ A) : Real.tanh x ∈ tanh R A

Soundness of tanh: membership is preserved by Real.tanh (via tanhBounds).

noncomputable def TorchLean.Floats.Interval.RInterval.sqrt (R : Rounder) (A : RInterval) : RInterval

Outward-rounded interval enclosure for Real.sqrt (requires $0\le\mathtt{lo}$).

theorem TorchLean.Floats.Interval.RInterval.mem_sqrt {R : Rounder} {A : RInterval} {x : ℝ} (hA : 0 ≤ A.lo) (hx : x ∈ A) : √x ∈ sqrt R A

Soundness of sqrt: membership is preserved by Real.sqrt when A is nonnegative.

noncomputable def TorchLean.Floats.Interval.RInterval.log (R : Rounder) (A : RInterval) : RInterval

Outward-rounded interval enclosure for Real.log (requires $0<\mathtt{lo}$).

theorem TorchLean.Floats.Interval.RInterval.mem_log {R : Rounder} {A : RInterval} {x : ℝ} (hA : 0 < A.lo) (hx : x ∈ A) : Real.log x ∈ log R A

Soundness of log: membership is preserved by Real.log on positive intervals.

Extended-real intervals (for division by an interval containing 0)

structure TorchLean.Floats.Interval.EInterval : Type

An EReal interval [lo,hi].

We use this for operations like division where a single interval may need to represent unbounded results (-∞/+∞) in a sound-but-coarse way.

• lo : EReal

  lo.

• hi : EReal

  hi.

def TorchLean.Floats.Interval.EInterval.mem (I : EInterval) (x : EReal) : Prop

Membership predicate: x ∈ I means I.lo ≤ x ≤ I.hi in EReal.

@[implicit_reducible]

instance TorchLean.Floats.Interval.EInterval.instMembershipEReal : Membership EReal EInterval

Enable x ∈ I notation for EReal intervals.

@[simp]

theorem TorchLean.Floats.Interval.EInterval.mem_iff (I : EInterval) (x : EReal) : x ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi

Unfold membership: x ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi.

noncomputable def TorchLean.Floats.Interval.EInterval.top : EInterval

Top interval [-∞,+∞] (the most conservative enclosure).

@[simp]

theorem TorchLean.Floats.Interval.EInterval.mem_top (x : EReal) : x ∈ top

Every value lies in top = [-∞,+∞].

@[inline]

def TorchLean.Floats.Interval.EInterval.ofRInterval (I : RInterval) : EInterval

Embed a real interval into an extended-real interval.

@[simp]

theorem TorchLean.Floats.Interval.EInterval.mem_ofRInterval (I : RInterval) (x : ℝ) : ↑x ∈ ofRInterval I ↔ x ∈ I

Membership in ofRInterval is the same as membership in the underlying real interval.

This is a small simp lemma that helps bridge between ℝ-level and EReal-level enclosures.

Division with overflow-awareness.

If the denominator interval contains 0, the result is unbounded ([-∞,+∞]). Otherwise we return a loose enclosure using absolute-value bounds.

noncomputable def TorchLean.Floats.Interval.RInterval.div (R : Rounder) (A B : RInterval) : EInterval

Outward-rounded interval division as an EReal enclosure.

If the denominator interval contains 0, we return EInterval.top = [-∞,+∞]. Otherwise we use a coarse-but-sound absolute-value bound and outward-round the endpoints with R.

theorem TorchLean.Floats.Interval.RInterval.mem_div_of_nozero {R : Rounder} {A B : RInterval} {x y : ℝ} (hx : x ∈ A) (hy : y ∈ B) (h0 : ¬(B.lo ≤ 0 ∧ 0 ≤ B.hi)) : ↑(x / y) ∈ div R A B

Soundness of div in the nonzero-denominator case (0 ∉ B).

Under the hypothesis ¬ (B.lo ≤ 0 ∧ 0 ≤ B.hi), the constructed EInterval contains the true real quotient x/y (as an EReal).