TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Interval.Finite

Configured interval enclosures for finite-only encodings #

Finite-only formats saturate on overflow. Unlike an IEEE interval with infinite endpoints, their whole range cannot enclose every real number. These theorems transport the existing model results with explicit range hypotheses on the exact endpoint calculations.

source
theorem FloatLib.Floats.ExecFloat.Binary.Interval.add_sound_of_encoding_finite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.encoding = Formats.BinaryInterchange.FloatFormat.Encoding.finite) (hloRange : |(Binary.toModel I.lo).toReal + (Binary.toModel J.lo).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (hhiRange : |(Binary.toModel I.hi).toReal + (Binary.toModel J.hi).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
(I.add J).RealMem (x + y)

Finite-only addition encloses a sum when the exact endpoint sums fit in the format.

source
theorem FloatLib.Floats.ExecFloat.Binary.Interval.sub_sound_of_encoding_finite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.encoding = Formats.BinaryInterchange.FloatFormat.Encoding.finite) (hloRange : |(Binary.toModel I.lo).toReal - (Binary.toModel J.hi).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (hhiRange : |(Binary.toModel I.hi).toReal - (Binary.toModel J.lo).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
(I.sub J).RealMem (x - y)

Finite-only subtraction encloses a difference when its endpoint differences fit in range.

source
theorem FloatLib.Floats.ExecFloat.Binary.Interval.mul_sound_of_encoding_finite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.encoding = Formats.BinaryInterchange.FloatFormat.Encoding.finite) (h00 : |(Binary.toModel I.lo).toReal * (Binary.toModel J.lo).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (h01 : |(Binary.toModel I.lo).toReal * (Binary.toModel J.hi).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (h10 : |(Binary.toModel I.hi).toReal * (Binary.toModel J.lo).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (h11 : |(Binary.toModel I.hi).toReal * (Binary.toModel J.hi).toReal| ≤ (Formats.BinaryInterchange.Model.posMaxFinite format).toReal) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
(I.mul J).RealMem (x * y)

Finite-only multiplication encloses a product when all four exact corner products fit.