TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.DirectedSemantics.Rational.Scaling

Exact real semantics of scaled natural rationals #

Scaled natural rationals provide the exact algebraic representation used by directed rational rounding. A rational is represented by natural numerator and denominator together with an external binary exponent. The shared exact Numerics.RationalBinary.scaleByPowerOfTwo operation moves that exponent into one side of the quotient; the main theorem proves that this transformation preserves the exact real value.

source
noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal (numerator denominator : ℕ) (exponent : ℤ) :
ℝ

Exact nonnegative real value represented by a scaled natural rational.

Instances For
    source
    noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.signedScaledRatToReal (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) :
    ℝ

    Apply a stored sign bit to the exact value of a scaled natural rational.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signedScaledRatToReal_eq_div_toReal (dx dy : Numerics.Dyadic) :
      signedScaledRatToReal (dx.negative ^^ dy.negative) dx.significand dy.significand (dx.exponent - dy.exponent) = dx.toReal / dy.toReal

      The signed scaled rational formed from two dyadics is their exact real quotient.

      The equality also covers a zero denominator because division in ℝ is totalized at zero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_mul_bpow_ofNat (numerator denominator shift : ℕ) :
      ↑numerator / ↑denominator * bpow (Int.ofNat shift) = ↑(numerator.shiftLeft shift) / ↑denominator

      Shifting the numerator realizes multiplication by a nonnegative binary power.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_mul_bpow_negSucc (numerator denominator shift : ℕ) :
      ↑numerator / ↑denominator * bpow (Int.negSucc shift) = ↑numerator / ↑(denominator.shiftLeft (shift + 1))

      Shifting the denominator realizes multiplication by a negative binary power.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleByPowerOfTwo_real (numerator denominator : ℕ) (exponent : ℤ) :
      ↑(Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).1 / ↑(Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).2 = scaledRatToReal numerator denominator exponent

      Moving a binary exponent into the numerator or denominator preserves the represented real ratio.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_nonneg (numerator denominator : ℕ) (exponent : ℤ) :
      0 ≤ scaledRatToReal numerator denominator exponent

      The unsigned scaled rational is nonnegative.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_pos (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) :
      0 < scaledRatToReal numerator denominator exponent

      The unsigned scaled rational is positive when both natural components are nonzero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_mul_bpow (numerator denominator : ℕ) (left right : ℤ) :
      scaledRatToReal numerator denominator left * bpow right = scaledRatToReal numerator denominator (left + right)

      Combining two external binary scales adds their exponents.