TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Interval.Arithmetic

Outward-rounded arithmetic for Model.Interval #

Each endpoint operation uses the corresponding directed Model kernel. Multiplication and division use the classical four-corner construction. Division returns the whole interval when the denominator contains zero because a single closed interval cannot represent the resulting disconnected quotient set. Addition, subtraction, multiplication, and division pass computed endpoints through ofBounds, replacing NaN or reversed endpoints with the format's whole range. For formats without infinity, enclosure of real results still requires the relevant range bounds.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add {fmt : FloatFormat} (A B : Interval fmt) :
Interval fmt

Outward-rounded interval addition.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.neg {fmt : FloatFormat} (A : Interval fmt) :
    Interval fmt

    Interval negation, reversing and negating the endpoints.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub {fmt : FloatFormat} (A B : Interval fmt) :
      Interval fmt

      Outward-rounded interval subtraction.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul {fmt : FloatFormat} (A B : Interval fmt) :
        Interval fmt

        Outward-rounded interval multiplication using all four endpoint products.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.div {fmt : FloatFormat} (A B : Interval fmt) :
          Interval fmt

          Outward-rounded interval division.

          When the denominator contains zero, the result is whole fmt; otherwise all four directed quotients determine the endpoint enclosure.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.inv {fmt : FloatFormat} (B : Interval fmt) :
            Interval fmt

            Interval reciprocal, conservatively returning whole fmt when zero is included.

            Instances For