TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.Format.Digits

Integer Digits, Scaling, and Slices #

These definitions are the effective integer layer used by radix-based rounding algorithms. Signed division and remainder use Int.tdiv and Int.tmod, matching Flocq's quotient and remainder toward zero rather than Lean's Euclidean / and % operations.

source
def FloatLib.Floats.Formats.Flocq.intPower (β : Numerics.Radix) (e : ℤ) :
ℤ

Integer radix power, with the Flocq convention that negative powers are zero.

Instances For
    source
    @[simp]
    theorem FloatLib.Floats.Formats.Flocq.intPower_of_nonneg (β : Numerics.Radix) {e : ℤ} (he : 0 ≤ e) :
    intPower β e = Int.ofNat (β.base ^ e.toNat)

    At nonnegative exponents, intPower is the ordinary natural radix power.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.Flocq.intPower_of_neg (β : Numerics.Radix) {e : ℤ} (he : e < 0) :
    intPower β e = 0

    At negative exponents, the integer radix-power convention returns zero.

    source
    theorem FloatLib.Floats.Formats.Flocq.intPower_zero (β : Numerics.Radix) :
    intPower β 0 = 1

    The zeroth integer radix power is one.

    source
    def FloatLib.Floats.Formats.Flocq.digit (β : Numerics.Radix) (n k : ℤ) :
    ℤ

    The signed radix digit at position k.

    Instances For
      source
      @[simp]
      theorem FloatLib.Floats.Formats.Flocq.digit_zero (β : Numerics.Radix) (k : ℤ) :
      digit β 0 k = 0

      Every radix digit of zero is zero.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.Flocq.digit_neg (β : Numerics.Radix) (n k : ℤ) :
      digit β (-n) k = -digit β n k

      Signed digit extraction commutes with integer negation.

      source
      theorem FloatLib.Floats.Formats.Flocq.digit_of_neg_index (β : Numerics.Radix) (n : ℤ) {k : ℤ} (hk : k < 0) :
      digit β n k = 0

      Integer digit positions below zero contain no digit.

      source
      theorem FloatLib.Floats.Formats.Flocq.digit_abs_lt_base (β : Numerics.Radix) (n k : ℤ) :
      |digit β n k| < Int.ofNat β.base

      Every signed digit has absolute value strictly smaller than the radix.

      source
      def FloatLib.Floats.Formats.Flocq.scale (β : Numerics.Radix) (n k : ℤ) :
      ℤ

      Shift an integer left for nonnegative k, and right with truncation for negative k.

      Instances For
        source
        theorem FloatLib.Floats.Formats.Flocq.scale_of_nonneg (β : Numerics.Radix) (n : ℤ) {k : ℤ} (hk : 0 ≤ k) :
        scale β n k = n * intPower β k

        A nonnegative scale multiplies by the corresponding radix power.

        source
        theorem FloatLib.Floats.Formats.Flocq.scale_of_neg (β : Numerics.Radix) (n : ℤ) {k : ℤ} (hk : k < 0) :
        scale β n k = n.tdiv (intPower β (-k))

        A negative scale divides toward zero by the corresponding positive radix power.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.Flocq.scale_zero_value (β : Numerics.Radix) (k : ℤ) :
        scale β 0 k = 0

        Scaling the zero value gives zero.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.Flocq.scale_zero_shift (β : Numerics.Radix) (n : ℤ) :
        scale β n 0 = n

        A zero-place scale leaves the integer unchanged.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.Flocq.scale_neg (β : Numerics.Radix) (n k : ℤ) :
        scale β (-n) k = -scale β n k

        Radix scaling commutes with integer negation.

        source
        def FloatLib.Floats.Formats.Flocq.slice (β : Numerics.Radix) (n start width : ℤ) :
        ℤ

        Extract width radix digits beginning at start; negative widths produce zero.

        Instances For
          source
          @[simp]
          theorem FloatLib.Floats.Formats.Flocq.slice_zero_value (β : Numerics.Radix) (start width : ℤ) :
          slice β 0 start width = 0

          Every radix slice of zero is zero.

          source
          theorem FloatLib.Floats.Formats.Flocq.slice_of_neg_width (β : Numerics.Radix) (n start : ℤ) {width : ℤ} (hwidth : width < 0) :
          slice β n start width = 0

          A negative-width radix slice is empty and therefore evaluates to zero.

          source
          theorem FloatLib.Floats.Formats.Flocq.slice_abs_lt_power (β : Numerics.Radix) (n start : ℤ) {width : ℤ} (hwidth : 0 ≤ width) :
          |slice β n start width| < intPower β width

          A nonnegative-width slice has absolute value below the corresponding radix power.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Flocq.slice_neg (β : Numerics.Radix) (n start width : ℤ) :
          slice β (-n) start width = -slice β n start width

          Radix slicing commutes with integer negation.

          source
          def FloatLib.Floats.Formats.Flocq.digits (β : Numerics.Radix) (n : ℤ) :
          ℕ

          Number of base-β digits in the absolute value of an integer.

          Instances For
            source
            @[simp]
            theorem FloatLib.Floats.Formats.Flocq.digits_zero (β : Numerics.Radix) :
            digits β 0 = 0

            Zero has no significant radix digits.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.Flocq.digits_neg (β : Numerics.Radix) (n : ℤ) :
            digits β (-n) = digits β n

            Radix digit count depends only on the integer's absolute value.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_pos {β : Numerics.Radix} {n : ℤ} (hn : n ≠ 0) :
            0 < digits β n

            Every nonzero integer has a positive radix digit count.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_bounds (β : Numerics.Radix) {n : ℤ} (hn : n ≠ 0) :
            β.base ^ (digits β n - 1) ≤ n.natAbs ∧ n.natAbs < β.base ^ digits β n

            A nonzero integer lies between consecutive powers selected by its digit count.

            source
            theorem FloatLib.Floats.Formats.Flocq.magnitude_intCast_of_pos (β : Numerics.Radix) {n : ℤ} (hn : 0 < n) :
            magnitude β ↑n = ↑(digits β n)

            The radix digit count of a positive integer is the magnitude of its real embedding.

            source
            theorem FloatLib.Floats.Formats.Flocq.intCast_lt_bpow_digits (β : Numerics.Radix) {n : ℤ} (hn : 0 < n) :
            ↑n < bpow β ↑(digits β n)

            A positive integer is strictly below the radix power selected by its digit count.

            source
            theorem FloatLib.Floats.Formats.Flocq.intCast_add_one_le_bpow_digits (β : Numerics.Radix) {n : ℤ} (hn : 0 < n) :
            ↑(n + 1) ≤ bpow β ↑(digits β n)

            The successor of a positive integer does not exceed its next radix-power boundary.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_unique (β : Numerics.Radix) {n : ℤ} (hn : n ≠ 0) {d : ℕ} (hd : 0 < d) (hlower : β.base ^ (d - 1) ≤ n.natAbs) (hupper : n.natAbs < β.base ^ d) :
            digits β n = d

            The power bounds uniquely determine the digit count of a nonzero integer.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_mono_abs (β : Numerics.Radix) {n m : ℤ} (hn : n ≠ 0) (hnm : n.natAbs ≤ m.natAbs) :
            digits β n ≤ digits β m

            Digit count is monotone with respect to integer absolute value away from zero.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_mul_le (β : Numerics.Radix) {n m : ℤ} (hn : n ≠ 0) (hm : m ≠ 0) :
            digits β (n * m) ≤ digits β n + digits β m

            A nonzero product uses at most the sum of the operand digit counts.

            source
            theorem FloatLib.Floats.Formats.Flocq.digits_power (β : Numerics.Radix) (k : ℕ) :
            digits β (Int.ofNat (β.base ^ k)) = k + 1

            A positive radix power has one more digit than its exponent.