TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.DirectedSemantics.Rational.Conversion

Exact rational conversion for directed Model rounding #

Normalized mathlib Rat values round directly into any Model fmt. For conventional IEEE formats, directed overflow returns either a signed infinity or the largest finite value of the same sign, according to the rounding direction. The conversion theorems establish the extended-real lower bound for downward conversion and non-NaN results in both directions.

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQWithRounding (fmt : FloatFormat) (mode : IEEERoundingMode) (q : ℚ) :
Model fmt

Round an exact rational according to an IEEE rounding direction.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQ (fmt : FloatFormat) (q : ℚ) :
    Model fmt

    Round an exact rational to nearest, ties to even.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQDown (fmt : FloatFormat) (q : ℚ) :
      Model fmt

      Round an exact rational toward negative infinity.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQUp (fmt : FloatFormat) (q : ℚ) :
        Model fmt

        Round an exact rational toward positive infinity.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundRatQDown_le (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
          (roundRatQDown fmt q).toEReal ≤ ↑↑q

          Downward conversion of an exact rational is an extended-real lower bound.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatQDown_eq_false (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
          (roundRatQDown fmt q).isNaN = false

          Downward conversion of a normalized rational never produces NaN.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatQUp_eq_false (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
          (roundRatQUp fmt q).isNaN = false

          Upward conversion of a normalized rational never produces NaN.