TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Interval.Runtime

Intervals with configured binary endpoints #

ExecFloat.Binary.Interval stores endpoints in the same carrier as configured scalar values. All operations delegate to Model.Interval; packing and decoding change representation, not rounding or exceptional-value behavior. The format, storage plan, and codec are unrestricted.

Arithmetic uses outward rounding and the model's whole-range fallback for unordered bounds. Valid requires finite endpoints; ValidExtended also permits infinities. The real-enclosure theorems and lossless-conversion proofs are in Configured.Interval.Proof.

source
@[reducible, inline]
abbrev FloatLib.Floats.ExecFloat.Binary.Interval {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} :
Type

A closed interval stored in the configured endpoint carrier.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.Interval.toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
    Formats.BinaryInterchange.Model.Interval format

    Decode both endpoints without changing their complete encodings.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Binary.Interval.ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Formats.BinaryInterchange.Model.Interval format) :
      Interval

      Pack both model endpoints into the configured carrier.

      Instances For
        source
        def FloatLib.Floats.ExecFloat.Binary.Interval.mem {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
        Prop

        Numerical membership; a NaN value or endpoint is unordered.

        Instances For
          source
          @[instance_reducible]
          instance FloatLib.Floats.ExecFloat.Binary.Interval.instMembershipFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
          Membership (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Interval

          Membership of a configured scalar in configured bounds.

          source
          @[reducible, inline]
          abbrev FloatLib.Floats.ExecFloat.Binary.Interval.Valid {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
          Prop

          Both endpoints are finite and ordered.

          Instances For
            source
            @[reducible, inline]
            abbrev FloatLib.Floats.ExecFloat.Binary.Interval.ValidExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
            Prop

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

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.Binary.Interval.point {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
              Interval

              Degenerate interval, preserving even a signed zero or NaN encoding.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.ExecFloat.Binary.Interval.whole {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
                Interval

                Complete numerical range: infinities where supported, maximal finite endpoints otherwise.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.ExecFloat.Binary.Interval.leB {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                  Bool

                  Executable numerical comparison; unordered comparisons return false.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.ExecFloat.Binary.Interval.ofBounds {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (lo hi : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    Interval

                    Keep ordered bounds, falling back to whole for NaNs or reversed endpoints.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.ExecFloat.Binary.Interval.containsZero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                      Bool

                      Test whether the numerical endpoint range contains zero.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.ExecFloat.Binary.Interval.hull {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
                        Interval

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

                        Instances For
                          source
                          @[inline]
                          def FloatLib.Floats.ExecFloat.Binary.Interval.add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
                          Interval

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

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Floats.ExecFloat.Binary.Interval.sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
                            Interval

                            Outward-rounded difference.

                            Instances For
                              source
                              @[inline]
                              def FloatLib.Floats.ExecFloat.Binary.Interval.mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
                              Interval

                              Outward-rounded four-corner product enclosure.

                              Instances For
                                source
                                @[inline]
                                def FloatLib.Floats.ExecFloat.Binary.Interval.div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
                                Interval

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

                                Instances For
                                  source
                                  @[inline]
                                  def FloatLib.Floats.ExecFloat.Binary.Interval.neg {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                                  Interval

                                  Negate and exchange the endpoints.

                                  Instances For
                                    source
                                    @[inline]
                                    def FloatLib.Floats.ExecFloat.Binary.Interval.inv {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                                    Interval

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

                                    Instances For
                                      source
                                      @[inline]
                                      def FloatLib.Floats.ExecFloat.Binary.Interval.relu {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                                      Interval

                                      Endpoint-grid image enclosure for max x 0.

                                      Instances For
                                        source
                                        @[inline]
                                        def FloatLib.Floats.ExecFloat.Binary.Interval.abs {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                                        Interval

                                        Absolute-value enclosure, handling intervals crossing zero.

                                        Instances For
                                          source
                                          @[inline]
                                          def FloatLib.Floats.ExecFloat.Binary.Interval.sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
                                          Interval

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

                                          Instances For