TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Interval.Operations

Powers and set operations for finite intervals #

Absolute values and even powers account for an interval crossing zero. Natural powers use mathlib's binary exponentiation on exact endpoints and round only the final bounds. Hull and intersection select existing endpoint encodings, so they introduce no further rounding.

As in Interval.Runtime, none reports an unavailable finite enclosure. Reciprocal requires a range strictly on one side of zero; intersection also fails when the ranges are disjoint.

source
def FloatLib.Numerics.Interval.absBounds {β : Type u_2} [Field β] [LinearOrder β] (I : Interval β) :
Interval β

Exact range of absolute value on an ordered interval.

Instances For
    source
    def FloatLib.Numerics.Interval.squareBounds {β : Type u_2} [Field β] [LinearOrder β] (I : Interval β) :
    Interval β

    Exact square bounds on an ordered interval, with lower bound zero if it crosses zero.

    Instances For
      source
      def FloatLib.Numerics.Interval.powBounds {β : Type u_2} [Field β] [LinearOrder β] (I : Interval β) (n : ℕ) :
      Interval β

      Exact natural-power bounds for an ordered interval, evaluated by repeated squaring.

      The zeroth power is [1, 1], including at zero. Even positive powers use the absolute-value range; odd powers preserve endpoint order.

      Instances For
        source
        def FloatLib.Numerics.Interval.abs? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I : Interval α) :
        Option (Interval α)

        Outward-rounded absolute value, accounting for zero-crossing ranges before rounding.

        Instances For
          source
          def FloatLib.Numerics.Interval.square? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I : Interval α) :
          Option (Interval α)

          Outward-rounded square using the dependent range of x * x, rather than two independent inputs.

          Instances For
            source
            def FloatLib.Numerics.Interval.pow? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I : Interval α) (n : ℕ) :
            Option (Interval α)

            Natural power using logarithmically many endpoint multiplications, then outward rounding.

            Instances For
              source
              def FloatLib.Numerics.Interval.min? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) :
              Option (Interval α)

              Outward-rounded pointwise minimum of two intervals.

              Instances For
                source
                def FloatLib.Numerics.Interval.max? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) :
                Option (Interval α)

                Outward-rounded pointwise maximum of two intervals.

                Instances For
                  source
                  def FloatLib.Numerics.Interval.inv? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I : Interval α) :
                  Option (Interval α)

                  Outward-rounded reciprocal, failing for a range containing zero or unavailable bounds.

                  Instances For
                    source
                    def FloatLib.Numerics.Interval.hull? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) :
                    Option (Interval α)

                    Smallest interval containing two finite ordered intervals.

                    The selected input encodings are preserved. Undecodable or reversed input bounds return none.

                    Instances For
                      source
                      def FloatLib.Numerics.Interval.intersect? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) :
                      Option (Interval α)

                      Intersection of two finite intervals, retaining the selected input encodings.

                      Disjoint, reversed, or undecodable bounds return none; touching endpoints give a point interval.

                      Instances For