Floating-Point Error Bounds

We collect small, compositional error bounds for TorchLean’s Flocq-style rounding model.

The lowest-level rounding interface lives in NN/Floats/NeuralFloat/Rounding/Core.lean: once you have a rounding mode $r:\mathbb{R}\to\mathbb{Z}$ that satisfies the usual “round-to-nearest” property, you get the familiar half-ULP bound for a single rounding step.

Here we package that core lemma into helper theorems that come up frequently in proofs, including the $\operatorname{fl}(x)=x(1+\delta)$ factorization.

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 TorchLean.Floats.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 TorchLean.Floats.ErrorBounds.relative_error_round_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : relativeError x (neuralRound rnd x) hx ≤ neuralUlp β fexp x / (2 * |x|)

Relative error bound for a single neural_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.

One-step bounds for common expressions

theorem TorchLean.Floats.ErrorBounds.round_add_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x y : ℝ) : |neuralRound rnd (x + y) - (x + y)| ≤ neuralUlp β fexp (x + y) / 2

Rounding error for a real addition.

This is the core half-ULP bound instantiated at the expression x + y.

theorem TorchLean.Floats.ErrorBounds.round_mul_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x y : ℝ) : |neuralRound rnd (x * y) - x * y| ≤ neuralUlp β fexp (x * y) / 2

Rounding error for a real multiplication.

This is the core half‑ULP bound instantiated at the expression x * y.

theorem TorchLean.Floats.ErrorBounds.round_div_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x y : ℝ) : |neuralRound rnd (x / y) - x / y| ≤ neuralUlp β fexp (x / y) / 2

Rounding error for a real division.

theorem TorchLean.Floats.ErrorBounds.round_fma_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x y z : ℝ) : |neuralRound rnd (x * y + z) - (x * y + z)| ≤ neuralUlp β fexp (x * y + z) / 2

Rounding error for a “fused multiply-add” style expression x*y + z (one rounding step).

theorem TorchLean.Floats.ErrorBounds.round_sqrt_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) : |neuralRound rnd √x - √x| ≤ neuralUlp β fexp √x / 2

Rounding error for Real.sqrt x (one rounding step).

theorem TorchLean.Floats.ErrorBounds.round_rsqrt_abs_error {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) : |neuralRound rnd (1 / √x) - 1 / √x| ≤ neuralUlp β fexp (1 / √x) / 2

Rounding error for 1 / Real.sqrt x (one rounding step).

theorem TorchLean.Floats.ErrorBounds.neural_round_relative_error_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ neuralUlp β fexp x / (2 * |x|) ∧ neuralRound 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$.