Floating-Point Error Bounds

Single-step rounding in FloatLib’s Flocq-style model satisfies absolute and relative error bounds.

Theory.Rounding.Core proves a half-ULP bound for every rounding function satisfying ValidRndToNearest.

The half-ULP bound yields relative-error forms, including the $\operatorname{fl}(x)=x(1+\delta)$ factorization. To bound the error of a single rounded operation such as round rnd (x + y), apply error_bound_ulp at the exact expression.

Bounds for dot products, matrix operations, and backward stability require a concrete evaluation order and format hypotheses. They belong with the corresponding algorithm rather than in this generic one-step rounding file.

References

• N. J. Higham, "Accuracy and Stability of Numerical Algorithms", SIAM, 2nd ed., 2002.
• D. Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic", ACM Computing Surveys, 1991.
• IEEE Std 754-2019, "IEEE Standard for Floating-Point Arithmetic" (for the intended meaning of rounding modes and ULP terminology).

Single Operation Error Bounds

noncomputable def FloatLib.Floats.Formats.Flocq.ErrorBounds.relativeError (exact computed : ℝ) : exact ≠ 0 → ℝ

Relative error for a nonzero exact value.

The proof argument prevents a computation with a nonzero error at exact value zero from being misreported as having zero relative error. Use an absolute-error statement when the exact value may vanish.

theorem FloatLib.Floats.Formats.Flocq.ErrorBounds.relative_error_round_ulp {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : relativeError x (round rnd x) hx ≤ ulp β fexp x / (2 * |x|)

Relative error bound for a single round step (ULP form).

This is the “divide the half-ULP absolute bound by |x|” version of the classic rounding model. It is often the easiest lemma to use when a proof is naturally phrased in relative terms.

theorem FloatLib.Floats.Formats.Flocq.ErrorBounds.round_relative_error_ulp {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ ulp β fexp x / (2 * |x|) ∧ round rnd x = x * (1 + δ)

Relative error factorisation for rounding, with a ULP-based bound.

This is the standard model $\operatorname{fl}(x)=x(1+\delta)$, with $|\delta|$ bounded using the ULP at $x$.