Integer-grid rounding guarantees

The rounded integer fixes every exact integer, satisfies the directed bounds, and lies within half a unit in either nearest mode. The midpoint theorems specify the tie choice, which an error bound alone would not determine.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.cast_roundInteger (mode : RoundingMode) (value : ℚ) : ↑(roundInteger mode value) = mode.roundSigned (decide (value < 0)) |value|

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_error_eq (mode : RoundingMode) (value : ℚ) : |↑(roundInteger mode value) - value| = |↑(mode.roundMagnitude (decide (value < 0)) |value|) - |value||

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_error_lt_one (mode : RoundingMode) (value : ℚ) : |↑(roundInteger mode value) - value| < 1

All five directions change a rational by strictly less than one integer unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_error_le_half (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (value : ℚ) : |↑(roundInteger mode value) - value| ≤ 1 / 2

The two nearest modes have at most one-half unit of error.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_of_nonneg (mode : RoundingMode) (value : ℚ) (h : 0 ≤ value) : roundInteger mode value = ↑(mode.roundMagnitude false value)

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_of_neg (mode : RoundingMode) (value : ℚ) (h : value < 0) : roundInteger mode value = -↑(mode.roundMagnitude true (-value))

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_intCast (mode : RoundingMode) (value : ℤ) : roundInteger mode ↑value = value

Exact integers are fixed in every direction, including either sign and zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.le_roundInteger_towardPositive (value : ℚ) : value ≤ ↑(roundInteger RoundingMode.towardPositive value)

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_towardNegative_le (value : ℚ) : ↑(roundInteger RoundingMode.towardNegative value) ≤ value

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.abs_roundInteger_towardZero_le (value : ℚ) : |↑(roundInteger RoundingMode.towardZero value)| ≤ |value|

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_nearestEven_midpoint (negative : Bool) (n : ℕ) : roundInteger RoundingMode.nearestEven (if negative = true then -(↑n + 1 / 2) else ↑n + 1 / 2) = have rounded := if n % 2 = 1 then ↑(n + 1) else ↑n; if negative = true then -rounded else rounded

The sign is applied after the even adjacent magnitude has been selected.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger_nearestAway_midpoint (negative : Bool) (n : ℕ) : roundInteger RoundingMode.nearestAway (if negative = true then -(↑n + 1 / 2) else ↑n + 1 / 2) = if negative = true then -↑(n + 1) else ↑(n + 1)