TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Transcendentals.FixedPoint

Fixed-point primitives for executable transcendental functions #

At scale n, the integer k represents k * 2^(-n). Multiplication and division round back to that scale with ties to even. The scale is explicit so each format can choose its own working precision. Approximation policy and constants live in Config.lean.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint :
Type

Number of fractional binary digits in a signed fixed-point representation.

An integer k at scale n represents k * 2^(-n).

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.scaleInt (fixed : FixedPoint) :
    ℤ

    The fixed-point scale as an integer exponent.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.pow2Int (exponent : ℕ) :
      ℤ

      Integer power of two.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.one (fixed : FixedPoint) :
        ℤ

        The fixed-point encoding of one.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.roundQuotientEven (numerator denominator : ℤ) :
          ℤ

          Round an integer quotient to nearest, ties to even.

          Callers provide a strictly positive denominator.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.roundDivPow2Even (value : ℤ) (shift : ℕ) :
            ℤ

            Divide by a power of two, rounding to nearest with ties to even.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.shiftPow2Even (value shift : ℤ) :
              ℤ

              Scale an integer by a signed power of two.

              Negative shifts use nearest-even division.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.mul (fixed : FixedPoint) (left right : ℤ) :
                ℤ

                Fixed-point multiplication, rounded back to the context's scale.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.div (fixed : FixedPoint) (numerator denominator : ℤ) :
                  ℤ

                  Fixed-point division by a positive denominator, rounded back to the context's scale.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.divByNat (_fixed : FixedPoint) (value : ℤ) (denominator : ℕ) :
                    ℤ

                    Divide a fixed-point value by a positive natural number.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.ofDyadic (fixed : FixedPoint) (value : Numerics.Dyadic) :
                      ℤ

                      Round an exact dyadic to the context's scale, with ties to even.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.toDyadic (fixed : FixedPoint) (value : ℤ) :
                        Numerics.Dyadic

                        Convert a signed fixed-point integer to an exact dyadic.

                        Instances For
                          source
                          def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.FixedPoint.evalPolyDesc (fixed : FixedPoint) (coefficients : List ℤ) (value : ℤ) :
                          ℤ

                          Evaluate descending fixed-point polynomial coefficients by Horner's method.

                          Each multiplication rounds back to the fixed-point scale. An empty coefficient list evaluates to zero.

                          Instances For