Directed integer rounding of nonnegative rational quotients

The quotient operations used by directed rational rounding satisfy format-independent order bounds. Floor rounding lies below the exact real quotient, ceiling rounding lies above it, and integer lower and upper thresholds are preserved in the expected directions. The ceiling is Numerics.roundQuotient .up. Whether a quotient is an exact tie, as nearest-away rounding needs to know, depends only on the rational it represents.

Natural quotient bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_le_roundQuotient_up (numerator denominator : ℕ) : numerator / denominator ≤ Numerics.roundQuotient Numerics.MagnitudeRounding.up numerator denominator

The floor quotient is no larger than the ceiling quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotient_up_le_div_add_one (numerator denominator : ℕ) : Numerics.roundQuotient Numerics.MagnitudeRounding.up numerator denominator ≤ numerator / denominator + 1

The ceiling quotient is at most one larger than the floor quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_mul_le_numerator (numerator denominator : ℕ) : numerator / denominator * denominator ≤ numerator

Multiplying the floor quotient back by its denominator does not exceed the numerator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.numerator_le_roundQuotient_up_mul (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : numerator ≤ Numerics.roundQuotient Numerics.MagnitudeRounding.up numerator denominator * denominator

Multiplying the ceiling quotient back by a nonzero denominator covers the numerator.

Exact real enclosure

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ceil_div_eq_roundQuotient_up (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : ⌈↑numerator / ↑denominator⌉ = Int.ofNat (Numerics.roundQuotient Numerics.MagnitudeRounding.up numerator denominator)

The executable natural ceiling is the exact integer ceiling of the represented real quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_div_le_div (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : ↑(numerator / denominator) ≤ ↑numerator / ↑denominator

The natural floor quotient lies below the exact real quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_le_natCast_roundQuotient_up (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : ↑numerator / ↑denominator ≤ ↑(Numerics.roundQuotient Numerics.MagnitudeRounding.up numerator denominator)

The exact real quotient lies below its natural ceiling quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_roundQuotDirected_false_le (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : ↑(roundQuotDirected false numerator denominator) ≤ ↑numerator / ↑denominator

Downward quotient rounding is a lower bound on the exact real quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_natCast_roundQuotDirected_true (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : ↑numerator / ↑denominator ≤ ↑(roundQuotDirected true numerator denominator)

Upward quotient rounding is an upper bound on the exact real quotient.

Exact rational invariance

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_eq_of_rat_eq (roundUp : Bool) (numerator denominator numerator' denominator' : ℕ) (hdenominator : denominator ≠ 0) (hdenominator' : denominator' ≠ 0) (hvalue : ↑numerator / ↑denominator = ↑numerator' / ↑denominator') : roundQuotDirected roundUp numerator denominator = roundQuotDirected roundUp numerator' denominator'

Directed quotient rounding depends only on the represented nonnegative rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_scaleByPowerOfTwo_add (roundUp : Bool) (numerator denominator : ℕ) (firstExponent secondExponent : ℤ) (hdenominator : denominator ≠ 0) : have first := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator firstExponent; have second := Numerics.RationalBinary.scaleByPowerOfTwo first.1 first.2 secondExponent; have combined := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (firstExponent + secondExponent); roundQuotDirected roundUp second.1 second.2 = roundQuotDirected roundUp combined.1 combined.2

Successive exact binary scalings may be combined before directed quotient rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.two_mul_mod_eq_iff_of_rat_eq (numerator denominator numerator' denominator' : ℕ) (hdenominator : denominator ≠ 0) (hdenominator' : denominator' ≠ 0) (hvalue : ↑numerator / ↑denominator = ↑numerator' / ↑denominator') : 2 * (numerator % denominator) = denominator ↔ 2 * (numerator' % denominator') = denominator'

Whether a quotient is an exact tie, twice its remainder equal to its denominator, depends only on the represented nonnegative rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.two_mul_mod_scaleByPowerOfTwo_add_iff (numerator denominator : ℕ) (firstExponent secondExponent : ℤ) (hdenominator : denominator ≠ 0) : have first := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator firstExponent; have second := Numerics.RationalBinary.scaleByPowerOfTwo first.1 first.2 secondExponent; have combined := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (firstExponent + secondExponent); 2 * (second.1 % second.2) = second.2 ↔ 2 * (combined.1 % combined.2) = combined.2

Successive exact binary scalings may be combined before testing for an exact quotient tie.

Preservation of integer thresholds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_roundQuotDirected_of_mul_le (roundUp : Bool) (numerator denominator lower : ℕ) (hdenominator : denominator ≠ 0) (hlower : lower * denominator ≤ numerator) : lower ≤ roundQuotDirected roundUp numerator denominator

An integer lower bound on a quotient survives either directed integer rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_le_of_lt_mul (roundUp : Bool) (numerator denominator upper : ℕ) (hdenominator : denominator ≠ 0) (hupper : numerator < upper * denominator) : roundQuotDirected roundUp numerator denominator ≤ upper

A strict integer upper bound on a quotient bounds either directed integer rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_le_roundQuotDirected_of_le_div (roundUp : Bool) (numerator denominator exponent : ℕ) (hdenominator : denominator ≠ 0) (hlower : ↑(pow2 exponent) ≤ ↑numerator / ↑denominator) : pow2 exponent ≤ roundQuotDirected roundUp numerator denominator

A real power-of-two lower bound survives either directed integer rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_le_pow2_of_div_lt (roundUp : Bool) (numerator denominator exponent : ℕ) (hdenominator : denominator ≠ 0) (hupper : ↑numerator / ↑denominator < ↑(pow2 exponent)) : roundQuotDirected roundUp numerator denominator ≤ pow2 exponent

A strict real power-of-two upper bound weakly bounds either directed integer rounding.