Quantized real intervals and unbounded division enclosures

Intervals are propagated over ℝ or EReal, then their endpoints are snapped outward to a chosen representable grid, a Flocq-style $(\beta,\mathtt{fexp})$ format.

The usual workflow is:

• start from a real interval $x\in[\mathtt{lo},\mathtt{hi}]$;
• propagate it through arithmetic or a monotone nonlinear function; and
• round each new endpoint outward with a Rounder.

The layer is meant for real-valued enclosure proofs, not bit-level IEEE execution. It therefore has no NaN payloads, signed-zero rules, or status flags.

Division returns an EReal interval so that a denominator interval containing zero can be enclosed by $[-\infty,+\infty]$.

References:

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

structure FloatLib.Floats.Interval.RInterval : Type

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

• lo : ℝ

  Lower endpoint.

• hi : ℝ

  Upper endpoint.

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

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

@[instance_reducible]

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

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

@[simp]

theorem FloatLib.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}$.

@[inline]

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

Degenerate interval $[x,x]$.

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

Membership in a point interval is equality.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

Outward-rounded interval subtraction, implemented as $A+(-B)$.

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

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

For a member of the interval, this bounds its absolute value. It is useful for even functions such as Real.cosh, whose maximum over an interval occurs at an endpoint of largest magnitude.

theorem FloatLib.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 FloatLib.Floats.Interval.RInterval.mul (R : Rounder) (A B : RInterval) : RInterval

Outward-rounded multiplication using the four products of the endpoint pairs.

theorem FloatLib.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 FloatLib.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 FloatLib.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 mul: every product of members lies between the rounded corner bounds.

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

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

theorem FloatLib.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 FloatLib.Floats.Interval.RInterval.tanh (R : Rounder) (A : RInterval) : RInterval

Outward-rounded interval enclosure for the monotone function Real.tanh.

theorem FloatLib.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.

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

Outward-rounded interval enclosure for Real.sqrt; informative when $0\le\mathtt{lo}$.

theorem FloatLib.Floats.Interval.RInterval.mem_sqrt {R : Rounder} {A : RInterval} {x : ℝ} (hx : x ∈ A) : √x ∈ sqrt R A

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

Real.sqrt is monotone on all of ℝ (it sends every nonpositive input to 0), so no sign hypothesis on A is needed; the nonnegativity remark on sqrt only describes when the enclosure is informative.

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

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

theorem FloatLib.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 FloatLib.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

  Lower endpoint.

• hi : EReal

  Upper endpoint.

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

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

@[instance_reducible]

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

Enable x ∈ I notation for EReal intervals.

@[simp]

theorem FloatLib.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 FloatLib.Floats.Interval.EInterval.top : EInterval

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

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

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

@[inline]

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

Embed a real interval into an extended-real interval.

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

Embedding an interval into EReal preserves membership of real values.

Division with possibly unbounded results.

If the denominator interval contains 0, the enclosure is [-∞,+∞]. Otherwise the quotient is enclosed by the four endpoint quotients.

noncomputable def FloatLib.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 outward-round the minimum and maximum of the four endpoint quotients.

theorem FloatLib.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).

theorem FloatLib.Floats.Interval.RInterval.mem_div {R : Rounder} {A B : RInterval} {x y : ℝ} (hx : x ∈ A) (hy : y ∈ B) : ↑(x / y) ∈ div R A B

Soundness of div without any hypothesis on the denominator interval.

When B contains zero the result is EInterval.top, which contains everything; otherwise this is mem_div_of_nozero. Division by zero itself is Lean's totalized x / 0 = 0, which the top interval also contains.