TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.DirectedSemantics.Positive

Positive directed rounding for arbitrary executable float formats #

The shift-based directed rounders used by Model are related to the independent Flocq-style real semantics at the scaled-mantissa boundary, before subnormal and normal values are packed into interchange fields.

All definitions are uniform in FloatFormat.

Independent directed semantics #

source
@[reducible, inline]
noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtDown (fmt : FloatFormat) (x : ℝ) :
ℝ

Round a real downward on the gradual-underflow grid of fmt, before overflow handling.

Instances For
    source
    @[reducible, inline]
    noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtUp (fmt : FloatFormat) (x : ℝ) :
    ℝ

    Round a real upward on the gradual-underflow grid of fmt, before overflow handling.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtDown_zero (fmt : FloatFormat) :
      roundAtDown fmt 0 = 0

      Downward rounding fixes zero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAtUp_zero (fmt : FloatFormat) :
      roundAtUp fmt 0 = 0

      Upward rounding fixes zero.

      Executable scaled-mantissa rounding #

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

      Floor a natural mantissa after expressing it at targetExponent.

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

        Ceil a natural mantissa after expressing it at targetExponent.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentUp_ne_zero (mantissa : ℕ) (exponent targetExponent : ℤ) (hm : mantissa ≠ 0) :
          roundMantissaAtExponentUp mantissa exponent targetExponent ≠ 0

          Ceiling alignment preserves nonzeroness of a positive mantissa.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentDown_le_up (mantissa : ℕ) (exponent targetExponent : ℤ) :
          roundMantissaAtExponentDown mantissa exponent targetExponent ≤ roundMantissaAtExponentUp mantissa exponent targetExponent

          Floor alignment never exceeds ceiling alignment at the same exponent.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentUp_le_down_add_one (mantissa : ℕ) (exponent targetExponent : ℤ) :
          roundMantissaAtExponentUp mantissa exponent targetExponent ≤ roundMantissaAtExponentDown mantissa exponent targetExponent + 1

          Ceiling alignment is at most one unit above floor alignment.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_scaledMagnitude (mantissa : ℕ) (exponent targetExponent : ℤ) :
          Flocq.floorRound (↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = Int.ofNat (roundMantissaAtExponentDown mantissa exponent targetExponent)

          Downward shifting computes the integer floor of a scaled positive dyadic.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ceil_scaledMagnitude (mantissa : ℕ) (exponent targetExponent : ℤ) :
          Flocq.ceilRound (↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = Int.ofNat (roundMantissaAtExponentUp mantissa exponent targetExponent)

          Upward shifting computes the integer ceiling of a scaled positive dyadic.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentDown_mul_bpow_le (mantissa : ℕ) (exponent targetExponent : ℤ) :
          ↑(roundMantissaAtExponentDown mantissa exponent targetExponent) * bpow targetExponent ≤ ↑mantissa * bpow exponent

          Floor alignment at any target exponent is a lower bound for the exact dyadic magnitude.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_roundMantissaAtExponentUp_mul_bpow (mantissa : ℕ) (exponent targetExponent : ℤ) :
          ↑mantissa * bpow exponent ≤ ↑(roundMantissaAtExponentUp mantissa exponent targetExponent) * bpow targetExponent

          Ceiling alignment at any target exponent is an upper bound for the exact dyadic magnitude.