TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.DirectedSemantics.Signed

Signed directed rounding for arbitrary executable float formats #

Signed floor and ceiling semantics follow from the positive scaled-mantissa results. For negative inputs, downward rounding uses the upward-rounded magnitude and upward rounding uses the downward-rounded magnitude. The final theorems lift these integer identities through round to exact real equations for nonzero dyadics when fmt.isIEEE = true.

Signed scaled mantissas #

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.roundSignedMantissaAtExponentDown (sign : Bool) (mantissa : ℕ) (exponent targetExponent : ℤ) :
ℤ

Signed mantissa selected by rounding a dyadic toward negative infinity.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.roundSignedMantissaAtExponentUp (sign : Bool) (mantissa : ℕ) (exponent targetExponent : ℤ) :
    ℤ

    Signed mantissa selected by rounding a dyadic toward positive infinity.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_scaledDyadic (sign : Bool) (mantissa : ℕ) (exponent targetExponent : ℤ) :
      Flocq.floorRound ((if sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = roundSignedMantissaAtExponentDown sign mantissa exponent targetExponent

      Signed floor rounding swaps to ceiling on the magnitude of a negative dyadic.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ceil_scaledDyadic (sign : Bool) (mantissa : ℕ) (exponent targetExponent : ℤ) :
      Flocq.ceilRound ((if sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = roundSignedMantissaAtExponentUp sign mantissa exponent targetExponent

      Signed ceiling rounding swaps to floor on the magnitude of a negative dyadic.

      Numerics.Dyadic rounded-real semantics #

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtDown_dyadic_eq (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) (hm : d.significand ≠ 0) :
      have target := fmt.toModel.targetExponent (Float.Model.totalExponent d.significand d.exponent); roundAtDown fmt d.toReal = ↑(roundSignedMantissaAtExponentDown d.negative d.significand d.exponent target) * Flocq.bpow Numerics.binaryRadix target

      Rounded-real semantics of downward rounding for a nonzero signed dyadic.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtUp_dyadic_eq (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) (hm : d.significand ≠ 0) :
      have target := fmt.toModel.targetExponent (Float.Model.totalExponent d.significand d.exponent); roundAtUp fmt d.toReal = ↑(roundSignedMantissaAtExponentUp d.negative d.significand d.exponent target) * Flocq.bpow Numerics.binaryRadix target

      Rounded-real semantics of upward rounding for a nonzero signed dyadic.