Quantized interval arithmetic (rounding-on-ℝ, 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 (β,fexp) format).

The main intended use is verification/bounding:

• You start from a real interval x ∈ [lo,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 ℝ/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 [lo,hi].

• lo : ℝ

  lo.

• hi : ℝ

  hi.

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

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

@[implicit_reducible]

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

Enable x ∈ 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 ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi.

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

Validity predicate: endpoints are ordered (lo ≤ 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: -[lo,hi] = [-hi,-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 |lo| |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 ∈ I, then |x| ≤ absMax I.

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

Loose-but-sound multiplication enclosure.

For x ∈ A, y ∈ B we have |x*y| ≤ absMax A * absMax B, hence x*y ∈ [-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: Real.tanh x ∈ [-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 ≤ 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 < 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).