TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.Interval.IEEEExec32

Binary32 certificate intervals #

TorchLean's IEEE execution certificates store binary32 endpoints. Interval32 selects that carrier from FloatLib's generic interval type; the arithmetic and soundness proofs are FloatLib's. Other endpoint formats can use FloatLib.Numerics.Interval directly, with the corresponding outward-rounding adapter. Binary intervals retain the model's whole-range fallback for unordered or indeterminate endpoint results.

source
@[reducible, inline]
abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 :
Type

FloatLib bounds with the binary32 endpoints used by IEEE execution certificates.

Instances For
    source
    @[reducible, inline]
    abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.toModel (x : Interval32) :
    FloatLib.Floats.Formats.BinaryInterchange.Model.Interval (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)

    Decode both endpoints without changing their complete encodings.

    Instances For
      source
      @[reducible, inline]
      abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.Valid (x : Interval32) :
      Prop

      Both endpoints are finite and ordered.

      Instances For
        source
        @[reducible, inline]
        abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.ValidExtended (x : Interval32) :
        Prop

        Both endpoints are non-NaN and ordered; infinities are permitted.

        Instances For
          source
          @[reducible, inline]
          abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.containsZero (x : Interval32) :
          Bool

          Test whether the numerical endpoint range contains zero.

          Instances For
            source
            @[reducible, inline]
            abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.hull (x y : Interval32) :
            Interval32

            Endpoint hull, inheriting the model's IEEE NaN propagation.

            Instances For
              source
              @[reducible, inline]
              abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.add (x y : Interval32) :
              Interval32

              Outward-rounded sum, with the model's conservative fallback for indeterminate bounds.

              Instances For
                source
                @[reducible, inline]
                abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.sub (x y : Interval32) :
                Interval32

                Outward-rounded difference.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.mul (x y : Interval32) :
                  Interval32

                  Outward-rounded four-corner product enclosure.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.div (x y : Interval32) :
                    Interval32

                    Outward-rounded quotient; a denominator containing zero returns the whole range.

                    Instances For
                      source
                      @[reducible, inline]
                      abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.neg (x : Interval32) :
                      Interval32

                      Negate and exchange the endpoints.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.inv (x : Interval32) :
                        Interval32

                        Reciprocal enclosure; an interval containing zero returns the whole range.

                        Instances For
                          source
                          @[reducible, inline]
                          abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.relu (x : Interval32) :
                          Interval32

                          Endpoint-grid image enclosure for max x 0.

                          Instances For
                            source
                            @[reducible, inline]
                            abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.abs (x : Interval32) :
                            Interval32

                            Absolute-value enclosure, handling intervals crossing zero.

                            Instances For
                              source
                              @[reducible, inline]
                              abbrev TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.sqrt (x : Interval32) :
                              Interval32

                              Directed square-root endpoints; real soundness additionally needs nonnegative input bounds.

                              Instances For