NF Elementwise Bounds: Unary Operations

theorem Proofs.RuntimeApprox.NFBackend.approxT_scale_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} (c : TorchLean.Floats.NF β fexp rnd) {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.scaleSpec xS (toSpec c)) (xR.scaleSpec c) (linfNorm (scaleBoundTensor eps c xR))

approxT bound for scaling by a runtime constant (scale_spec) over arbitrary tensor shapes.

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

theorem Proofs.RuntimeApprox.NFBackend.approxT_neg_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.negSpec xS) xR.negSpec (linfNorm (negBoundTensor eps xR))

approxT bound for elementwise negation (neg_spec) over arbitrary tensor shapes.

theorem Proofs.RuntimeApprox.NFBackend.approxT_abs_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.absSpec xS) xR.absSpec (linfNorm (absBoundTensor eps xR))

approxT bound for elementwise absolute value (abs_spec) over arbitrary tensor shapes.

theorem Proofs.RuntimeApprox.NFBackend.approxT_exp_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.expSpec xS) xR.expSpec (linfNorm (expBoundTensor eps xR))

approxT bound for elementwise exponentiation (exp_spec) over arbitrary tensor shapes.

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

theorem Proofs.RuntimeApprox.NFBackend.approxT_tanh_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec MathFunctions.tanh xS) (Spec.Tensor.mapSpec MathFunctions.tanh xR) (linfNorm (tanhBoundTensor eps xR))

approxT 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 {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (x : TorchLean.Floats.NF β fexp rnd) : TorchLean.Floats.NF β fexp rnd

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

noncomputable def Proofs.RuntimeApprox.NFBackend.reluBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (xR : Spec.Tensor (TorchLean.Floats.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.approxT_relu_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec (fun (x : Spec.SpecScalar) => max x 0) xS) (Spec.Tensor.mapSpec reluR xR) (linfNorm (reluBoundTensor eps xR))

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

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