NF Elementwise Bounds: Unary Operations

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_scale_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} (c : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) {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.scaleSpec xS (toSpec c)) (xR.scaleSpec c) (linfNorm (scaleBoundTensor eps c xR))

approxTensor bound for scaling by a runtime constant (scaleSpec) over arbitrary tensor shapes.

This is the tensor-level wrapper around the scalar scaling lemma approx_scale_nf.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_scale_spec_of_approx {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} (cS : ℝ) (cR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps epsC : ℝ} : approxTensor toSpec xS xR eps → |toSpec cR - cS| ≤ epsC → approxTensor toSpec (TorchLean.Tensor.scaleSpec xS cS) (xR.scaleSpec cR) (linfNorm (scaleApproxBoundTensor eps epsC cR xR))

Tensor scaling with an approximate runtime coefficient.

If xR approximates xS by eps and the runtime coefficient cR approximates cS by epsC, then this theorem accounts for both perturbations and the final rounded multiplication. It is the coefficient-aware counterpart of approxTensor_scale_spec.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_neg_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.negSpec xS) xR.negSpec (linfNorm (negBoundTensor eps xR))

approxTensor bound for elementwise negation (negSpec) over arbitrary tensor shapes.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_abs_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.absSpec xS) xR.absSpec (linfNorm (absBoundTensor eps xR))

approxTensor bound for elementwise absolute value (absSpec) over arbitrary tensor shapes.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_exp_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.expSpec xS) xR.expSpec (linfNorm (expBoundTensor eps xR))

approxTensor bound for elementwise exponentiation (expSpec) over arbitrary tensor shapes.

This lifts the scalar mean-value-theorem bound approx_exp_nf.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_sqrt_spec_of_pos_lb {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} (η : ℝ) (hη : 0 < η) {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} : approxTensor toSpec xS xR eps → TorchLean.Tensor.Forall (fun (x : ℝ) => η ≤ x) xS → eps < η → approxTensor toSpec (TorchLean.Tensor.sqrtSpec xS) xR.sqrtSpec (linfNorm (sqrtPosBoundTensor η eps xR))

Shape-generic square-root approximation on a certified positive tensor domain.

The pointwise lower bound is carried by Tensor.Forall; the global condition eps < η guarantees that every rounded input remains positive. The output budget is assembled entrywise and reduced by the same infinity norm used throughout approxTensor.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_tanh_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.mapSpec MathFunctions.tanh xS) (TorchLean.Tensor.mapSpec MathFunctions.tanh xR) (linfNorm (tanhBoundTensor eps xR))

approxTensor bound for elementwise hyperbolic tangent (tanh) over arbitrary tensor shapes.

Currently uses the coarse unconditional scalar bound approx_tanh_nf (boundedness of tanh).

noncomputable def Proofs.RuntimeApprox.NFBackend.reluR {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (x : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd

Rounded ReLU scalar op for NF: apply max · 0 then round.

noncomputable def Proofs.RuntimeApprox.NFBackend.reluBoundTensor {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for ReLU (max · 0).

ReLU is 1-Lipschitz (|max x 0 - max y 0| ≤ |x - y|), so the only new error is the final rounding step in reluR.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_relu_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.mapSpec (fun (x : Spec.SpecScalar) => max x 0) xS) (TorchLean.Tensor.mapSpec reluR xR) (linfNorm (reluBoundTensor eps xR))

approxTensor bound for elementwise ReLU (max · 0) over arbitrary tensor shapes.

Combines the 1-Lipschitz property of max with one rounding step for reluR.