TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Capabilities.Radix

Positional-radix capability #

A radix is the base used by a positional numerical system. Binary floating point uses radix two, decimal floating point uses radix ten, and the abstract rounded-real development can work with any natural radix at least two.

This definition belongs to the general numerical layer: fixed point, floating point, and other positional systems can all use the same radix without depending on a binary storage format.

source
structure FloatLib.Numerics.Radix :
Type

A positional radix whose natural base is at least two.

  • base : ℕ

    Natural base of the positional system.

  • base_valid : 2 ≤ self.base

    Positional systems require a base of at least two.

Instances For
    source
    def FloatLib.Numerics.binaryRadix :
    Radix

    Binary radix.

    Instances For
      source
      def FloatLib.Numerics.decimalRadix :
      Radix

      Decimal radix.

      Instances For
        source
        def FloatLib.Numerics.Radix.toReal (radix : Radix) :
        ℝ

        View the radix as a real scaling factor.

        Instances For
          source
          theorem FloatLib.Numerics.Radix.pos (radix : Radix) :
          0 < radix.toReal

          Every radix is positive when interpreted as a real scaling factor.

          source
          theorem FloatLib.Numerics.Radix.ne_zero (radix : Radix) :
          radix.toReal ≠ 0

          A radix is nonzero when interpreted as a real scaling factor.

          source
          theorem FloatLib.Numerics.Radix.gt_one (radix : Radix) :
          1 < radix.toReal

          Every positional radix is strictly greater than one.