NF Elementwise Bounds: Binary Arithmetic

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_add_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {xS yS : Spec.SpecTensor s} {xR yR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {epsx epsy : ℝ} : approxTensor toSpec xS xR epsx → approxTensor toSpec yS yR epsy → approxTensor toSpec (TorchLean.Tensor.addSpec xS yS) (xR.addSpec yR) (linfNorm (addBoundTensor epsx epsy xR yR))

approxTensor bound for elementwise addition (addSpec) 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.approxTensor_sub_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {xS yS : Spec.SpecTensor s} {xR yR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {epsx epsy : ℝ} : approxTensor toSpec xS xR epsx → approxTensor toSpec yS yR epsy → approxTensor toSpec (TorchLean.Tensor.subSpec xS yS) (xR.subSpec yR) (linfNorm (subBoundTensor epsx epsy xR yR))

approxTensor bound for elementwise subtraction (subSpec) over arbitrary tensor shapes.

This is obtained by lifting the scalar subtraction bound approx_sub_nf via approxTensor_map2_spec_of_scalar_bound.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_mul_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {xS yS : Spec.SpecTensor s} {xR yR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {epsx epsy : ℝ} : approxTensor toSpec xS xR epsx → approxTensor toSpec yS yR epsy → approxTensor toSpec (TorchLean.Tensor.mulSpec xS yS) (xR.mulSpec yR) (linfNorm (mulBoundTensor epsx epsy xR yR))

approxTensor bound for elementwise multiplication (mulSpec) over arbitrary tensor shapes.

The scalar core is approx_mul_nf, lifted componentwise; the resulting bound is packaged as mulBoundTensor and reduced with linfNorm.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_square_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} : approxTensor toSpec xS xR eps → approxTensor toSpec (TorchLean.Tensor.squareSpec xS) xR.squareSpec (linfNorm (mulBoundTensor eps eps xR xR))

Squaring is the diagonal specialization of elementwise multiplication, so it uses the same rounded multiplication bound rather than a separate numerical rule.