Upward bounds for directed rational packing #
For a positive exact rational and a descriptor with fmt.isIEEE = true, the executable upward
rounder returns positive infinity or a finite value no smaller than the input.
Upward normal rounding may carry into a new exponent and may overflow. The branch lemmas cover
both cases. The final EReal inequality includes positive infinity and supplies the upper bound
used by the directed-rounding semantics.
Positive upward bounds #
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_up_eq_posInf_or_finite_ge
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent = posInf fmt ∨ (roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent).isFinite = true ∧ scaledRatToReal numerator denominator exponent ≤ (roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent).toReal
Positive upward rational rounding is either positive infinity or a finite value no smaller than the exact scaled rational.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatMagnitudeDirectedScaled_pos_up_eq_false
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
Positive upward rational rounding is never classified as NaN.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_roundRatMagnitudeDirectedScaled_pos_up
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
↑(scaledRatToReal numerator denominator exponent) ≤ (roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent).toEReal
Positive upward rational rounding is an upper bound in the extended reals.