Soundness of partial, representation-independent interval arithmetic

Every theorem retains the successful-result hypothesis. Failed decoding, unavailable outward rounding, and zero-crossing division are not interpreted as valid finite enclosures.

theorem FloatLib.Numerics.Interval.decode?_eq_some_iff {α : Type u_1} {β : Type u_2} (decode : α → Option β) (I : Interval α) (a : Interval β) : decode? decode I = some a ↔ decode I.lo = some a.lo ∧ decode I.hi = some a.hi

Successful interval decoding determines each endpoint interpretation.

theorem FloatLib.Numerics.Interval.contains_iff_of_decode? {α : Type u_1} {β : Type u_2} [LinearOrder β] {decode : α → Option β} {I : Interval α} {a : Interval β} (ha : decode? decode I = some a) (x : β) : Contains decode I x ↔ a.lo ≤ x ∧ x ≤ a.hi

After successful decoding, membership is the ordinary closed-interval predicate.

theorem FloatLib.Numerics.Interval.contains_encloseInterval? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) {a : Interval β} {I : Interval α} (h : encloseInterval? R a = some I) {x : β} (hx : a.lo ≤ x ∧ x ≤ a.hi) : Contains R.decode I x

Outward rounding of the endpoint pair encloses every member of the exact interval.

theorem FloatLib.Numerics.Interval.contains_liftUnary? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (f : Interval β → Interval β) (g : β → β) (hf : ∀ (a : Interval β) (x : β), a.lo ≤ x ∧ x ≤ a.hi → (f a).lo ≤ g x ∧ g x ≤ (f a).hi) {I K : Interval α} (h : liftUnary? R f I = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K (g x)

Any sound exact unary endpoint enclosure lifts through partial outward rounding.

theorem FloatLib.Numerics.Interval.contains_liftBinary? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (f : Interval β → Interval β → Interval β) (g : β → β → β) (hf : ∀ (a b : Interval β) (x y : β), a.lo ≤ x ∧ x ≤ a.hi → b.lo ≤ y ∧ y ≤ b.hi → (f a b).lo ≤ g x y ∧ g x y ≤ (f a b).hi) {I J K : Interval α} (h : liftBinary? R f I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (g x y)

Any sound exact binary endpoint enclosure lifts through partial outward rounding.

theorem FloatLib.Numerics.Interval.contains_neg? {α : Type u_1} {β : Type u_2} [LinearOrder β] [Field β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I K : Interval α} (h : neg? R I = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K (-x)

Every successful negation encloses the exact negative value.

theorem FloatLib.Numerics.Interval.contains_add? {α : Type u_1} {β : Type u_2} [LinearOrder β] [Field β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I J K : Interval α} (h : add? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (x + y)

Every successful addition encloses the exact sum.

theorem FloatLib.Numerics.Interval.contains_sub? {α : Type u_1} {β : Type u_2} [LinearOrder β] [Field β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I J K : Interval α} (h : sub? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (x - y)

Every successful subtraction encloses the exact difference.

theorem FloatLib.Numerics.Interval.contains_mul? {α : Type u_1} {β : Type u_2} [LinearOrder β] [Field β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I J K : Interval α} (h : mul? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (x * y)

Every successful four-corner multiplication encloses the exact product.

theorem FloatLib.Numerics.Interval.contains_div? {α : Type u_1} {β : Type u_2} [LinearOrder β] [Field β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I J K : Interval α} (h : div? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (x / y)

Successful division certifies a nonzero denominator range and encloses the exact quotient.