Numerical guarantees for exact coefficient rounding

The computed coefficient fixes nonnegative integers, brackets the exact magnitude, satisfies directed inequalities, and has at most half a grid unit of error in either nearest mode.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.increment_zero (mode : RoundingMode) (s : Bool) (n : ℕ) : mode.increment s n 0 = false

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_natCast (mode : RoundingMode) (s : Bool) (n : ℕ) : mode.roundMagnitude s ↑n = n

Every nonnegative integer is fixed in every rounding direction.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_eq_floor_or_succ (mode : RoundingMode) (s : Bool) (x : ℚ) : mode.roundMagnitude s x = ⌊x⌋₊ ∨ mode.roundMagnitude s x = ⌊x⌋₊ + 1

The rounded coefficient is one of the two adjacent integer grid points.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.floor_le_roundMagnitude (mode : RoundingMode) (s : Bool) (x : ℚ) : ⌊x⌋₊ ≤ mode.roundMagnitude s x

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_le_floor_add_one (mode : RoundingMode) (s : Bool) (x : ℚ) : mode.roundMagnitude s x ≤ ⌊x⌋₊ + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_error_lt_one (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.roundMagnitude s x) - x| < 1

A directed or nearest rounding changes a nonnegative value by less than one grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_error_le_half (mode : RoundingMode) (hm : mode = nearestEven ∨ mode = nearestAway) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.roundMagnitude s x) - x| ≤ 1 / 2

Both nearest modes have an error of at most half an integer grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_towardZero_le (s : Bool) {x : ℚ} (hx : 0 ≤ x) : ↑(towardZero.roundMagnitude s x) ≤ x

Rounding toward zero does not increase magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.le_roundMagnitude_towardPositive {x : ℚ} (hx : 0 ≤ x) : x ≤ ↑(towardPositive.roundMagnitude false x)

Positive upward rounding is an upper enclosure.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.le_roundSigned_towardPositive (s : Bool) {x : ℚ} (hx : 0 ≤ x) : (if s = true then -x else x) ≤ towardPositive.roundSigned s x

Upward rounding is an upper enclosure for either sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundSigned_towardNegative_le (s : Bool) {x : ℚ} (hx : 0 ≤ x) : towardNegative.roundSigned s x ≤ if s = true then -x else x

Downward rounding is a lower enclosure for either sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_nearestEven_midpoint (s : Bool) (n : ℕ) : nearestEven.roundMagnitude s (↑n + 1 / 2) = if n % 2 = 1 then n + 1 else n

At an exact midpoint, nearest-even chooses the even adjacent coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_nearestAway_midpoint (s : Bool) (n : ℕ) : nearestAway.roundMagnitude s (↑n + 1 / 2) = n + 1

Nearest-away increases magnitude at every exact midpoint, for either sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundAt_error_lt_one (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (q : ℤ) : |↑(mode.roundAt s x q) * 10 ^ q - x| < 10 ^ q

All five modes have strictly less than one decimal grid unit of error.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundAt_error_le_half (mode : RoundingMode) (hm : mode = nearestEven ∨ mode = nearestAway) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (q : ℤ) : |↑(mode.roundAt s x q) * 10 ^ q - x| ≤ 10 ^ q / 2

The error bound scales by the actual decimal quantum, for any exponent.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundAt_exact (mode : RoundingMode) (s : Bool) (c : ℕ) {q r : ℤ} (h : r ≤ q) : mode.roundAt s (↑c * 10 ^ q) r = c * 10 ^ (q - r).toNat

A finite decimal remains exact on every finer decimal grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundAt_exact_value (mode : RoundingMode) (s : Bool) (c : ℕ) {q r : ℤ} (h : r ≤ q) : ↑(mode.roundAt s (↑c * 10 ^ q) r) * 10 ^ r = ↑c * 10 ^ q

Exact grid refinement preserves value in all five modes.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude_le_nat (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (n : ℕ) (hn : x ≤ ↑n) : mode.roundMagnitude s x ≤ n

An integer upper bound on the magnitude remains an upper bound after any rounding.