TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Exact rational conversion for directed Model rounding #

Model.ofRat fmt q rounds a normalized mathlib Rat once into any Model fmt, to nearest with ties to even. (mode := .up) selects another direction and (status := true) adds the IEEE exception flags and the ternary value. 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 and upper bounds and non-NaN results in both directions.

source
@[macro_inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.ofRat (fmt : FloatFormat) (q : ℚ) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) :
match status with | true => IEEEOutcome fmt | false => Model fmt

Round an exact rational once into fmt, in the direction mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value of that rounding.

Instances For
    source
    @[simp]
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_ofRat (fmt : FloatFormat) (q : ℚ) (mode : IEEERoundingMode) :
    (ofRat fmt q mode true).value = ofRat fmt q mode

    Rounding a rational with status := true delivers the value of the same rounding.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_ofRat_down_le (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
    toEReal (ofRat fmt q IEEERoundingMode.down) ≤ ↑↑q

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

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_ofRat_up (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
    ↑↑q ≤ toEReal (ofRat fmt q IEEERoundingMode.up)

    Upward conversion of an exact rational is an extended-real upper bound, including zero, subnormal rounding, and overflow to positive infinity.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_ofRat_down_eq_false (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
    isNaN (ofRat fmt q IEEERoundingMode.down) = false

    Downward conversion of a normalized rational never produces NaN.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_ofRat_up_eq_false (fmt : FloatFormat) (q : ℚ) (hfmt : fmt.isIEEE = true) :
    isNaN (ofRat fmt q IEEERoundingMode.up) = false

    Upward conversion of a normalized rational never produces NaN.