NF Elementwise Bounds: Binary Arithmetic #
theorem
Proofs.RuntimeApprox.NFBackend.approxT_add_spec
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{s : Spec.Shape}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{xS yS : Spec.SpecTensor s}
{xR yR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{epsx epsy : ℝ}
:
approxT toSpec xS xR epsx →
approxT toSpec yS yR epsy →
approxT toSpec (Spec.Tensor.addSpec xS yS) (xR.addSpec yR) (linfNorm (addBoundTensor epsx epsy xR yR))
approxT bound for elementwise addition (add_spec) over arbitrary tensor shapes.
The output epsilon is computed as linf_norm (add_bound_tensor epsx epsy xR yR), which combines the
input epsilons and one rounding-ULP term per element.
theorem
Proofs.RuntimeApprox.NFBackend.approxT_sub_spec
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{s : Spec.Shape}
{xS yS : Spec.SpecTensor s}
{xR yR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{epsx epsy : ℝ}
:
approxT toSpec xS xR epsx →
approxT toSpec yS yR epsy →
approxT toSpec (Spec.Tensor.subSpec xS yS) (xR.subSpec yR) (linfNorm (subBoundTensor epsx epsy xR yR))
approxT bound for elementwise subtraction (sub_spec) over arbitrary tensor shapes.
This is obtained by lifting the scalar subtraction bound approx_sub_nf via
approxT_map2_spec_of_scalar_bound.
theorem
Proofs.RuntimeApprox.NFBackend.approxT_mul_spec
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{s : Spec.Shape}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{xS yS : Spec.SpecTensor s}
{xR yR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{epsx epsy : ℝ}
:
approxT toSpec xS xR epsx →
approxT toSpec yS yR epsy →
approxT toSpec (Spec.Tensor.mulSpec xS yS) (xR.mulSpec yR) (linfNorm (mulBoundTensor epsx epsy xR yR))
approxT bound for elementwise multiplication (mul_spec) over arbitrary tensor shapes.
The scalar core is approx_mul_nf, lifted componentwise; the resulting bound is packaged as
mul_bound_tensor and reduced with linf_norm.