Error Bounds for General Rounding Modes

A valid rounding mode selects one of the two adjacent representable values. Consequently its absolute error is at most one ULP. Nearest rounding sharpens this to half an ULP; this file records the one-ULP result needed for directed and toward-zero modes.

theorem FloatLib.Floats.Formats.Flocq.round_abs_error_le_ulp {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : |round rnd x - x| ≤ ulp β fexp x

Every valid generic rounding mode has absolute error at most one ULP.

theorem FloatLib.Floats.Formats.Flocq.round_abs_error_lt_ulp_of_inexact {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x : ℝ} (hinexact : round rnd x ≠ x) : |round rnd x - x| < ulp β fexp x

A non-exact valid rounding has error strictly smaller than one ULP.

theorem FloatLib.Floats.Formats.Flocq.relative_error_round_FLX_of_valid {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : x ≠ 0) : ErrorBounds.relativeError x (round rnd x) hx ≤ bpow β (1 - prec)

Every valid FLX rounding mode has relative error at most β^(1-prec).

theorem FloatLib.Floats.Formats.Flocq.round_relative_error_FLX_of_valid {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ bpow β (1 - prec) ∧ round rnd x = x * (1 + δ)

General FLX rounding admits a multiplicative error model with a one-ULP relative bound.