TorchLean API

Docs HomeGuideExamplesGraphs

NN.Floats.IEEEExec.ErrorBounds

IEEE32Exec per-op real error bounds (finite branch) #

NN.Floats.IEEEExec.BridgeFP32Total provides refinement theorems of the form

toReal (op_exec x y) = fp32Round (op_real (toReal x) (toReal y)),

valid when the executable result stays finite (no NaN/Inf).

This file turns those equalities into the standard half-ULP absolute error bounds you want in numerical proofs:

|toReal (op_exec x y) - op_real (toReal x) (toReal y)| ≤ eps₃₂ (op_real (toReal x) (toReal y)).

We intentionally do not provide bounds for sin/cos here: the current executable implementation is deterministic (see NN.Floats.IEEEExec.Exec32), but it is an algorithmic approximation rather than “real trig + one rounding step”, so its real-analytic error bounds live in a separate trig-specific theory file.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_abs_error (x : ℝ) :
|fp32Round x - x| ≤ eps₃₂ x

fp32Round has the standard half-ULP absolute error bound.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.add y).isFinite = true) :
|(x.add y).toReal - (x.toReal + y.toReal)| ≤ eps₃₂ (x.toReal + y.toReal)

Addition absolute error bound for IEEE32Exec on the finite branch.

Informal: if add x y stays finite then |toReal(add x y) - (toReal x + toReal y)| ≤ eps₃₂(toReal x + toReal y).

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.mul y).isFinite = true) :
|(x.mul y).toReal - x.toReal * y.toReal| ≤ eps₃₂ (x.toReal * y.toReal)

Multiplication absolute error bound for IEEE32Exec on the finite branch.

Informal: if mul x y stays finite then |toReal(mul x y) - (toReal x * toReal y)| ≤ eps₃₂(toReal x * toReal y).

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.div y).isFinite = true) :
|(x.div y).toReal - x.toReal / y.toReal| ≤ eps₃₂ (x.toReal / y.toReal)

Division absolute error bound for IEEE32Exec on the finite branch.

Informal: if div x y stays finite then |toReal(div x y) - (toReal x / toReal y)| ≤ eps₃₂(toReal x / toReal y).

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_abs_error_of_isFinite (x y z : IEEE32Exec) (hfin : (x.fma y z).isFinite = true) :
|(x.fma y z).toReal - (x.toReal * y.toReal + z.toReal)| ≤ eps₃₂ (x.toReal * y.toReal + z.toReal)

FMA absolute error bound for IEEE32Exec on the finite branch.

Informal: if fma x y z stays finite then |toReal(fma x y z) - (toReal x * toReal y + toReal z)| ≤ eps₃₂(toReal x * toReal y + toReal z).

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_abs_error_of_isFinite (x : IEEE32Exec) (hfin : x.sqrt.isFinite = true) :
|x.sqrt.toReal - √x.toReal| ≤ eps₃₂ √x.toReal

Square-root absolute error bound for IEEE32Exec on the finite branch.

Informal: if sqrt x stays finite then |toReal(sqrt x) - Real.sqrt(toReal x)| ≤ eps₃₂(Real.sqrt(toReal x)).