NF Elementwise Bounds: Safe Division and Sigmoid

noncomputable def Proofs.RuntimeApprox.NFBackend.safeDiv (ε x y : ℝ) : ℝ

Spec-side safe division with a clamped denominator.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeDivR {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (ε : ℝ) (xR yR : TorchLean.Floats.NF β fexp rnd) : TorchLean.Floats.NF β fexp rnd

Runtime implementation of safeDiv as a single rounded primitive.

theorem Proofs.RuntimeApprox.NFBackend.approx_safeDiv_nf {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {x y : ℝ} {xR yR : TorchLean.Floats.NF β fexp rnd} {epsx epsy ε : ℝ} (hε : 0 < ε) (hx : |toSpec xR - x| ≤ epsx) (hy : |toSpec yR - y| ≤ epsy) : |toSpec (safeDivR ε xR yR) - safeDiv ε x y| ≤ 1 / ε * epsx + (|toSpec xR| + epsx) * (epsy / (ε * ε)) + TorchLean.Floats.neuralUlp β fexp (safeDiv ε (toSpec xR) (toSpec yR)) / 2

Forward approximation bound for safeDiv in NF.

safeDiv ε x y = x / max y ε clamps the denominator away from 0. For ε > 0, this yields an unconditional bound with explicit (1/ε) and (1/ε^2) sensitivity terms plus one rounding-ULP term.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeDivBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (ε epsx epsy : ℝ) (xR yR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for safeDiv.

This is the elementwise lifting of approx_safeDiv_nf's bound (with a max-clamped denominator).

theorem Proofs.RuntimeApprox.NFBackend.approxT_safeDiv_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} (ε : ℝ) (hε : 0 < ε) {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.map2Spec (safeDiv ε) xS yS) (Spec.Tensor.map2Spec (safeDivR ε) xR yR) (linfNorm (safeDivBoundTensor ε epsx epsy xR yR))

approxT bound for safeDiv lifted to arbitrary tensor shapes.

This is the tensor-level wrapper around approx_safeDiv_nf, built via approxT_map2_spec_of_scalar_bound.

noncomputable def Proofs.RuntimeApprox.NFBackend.sigmoidBoundScalar {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (xR : TorchLean.Floats.NF β fexp rnd) : ℝ

Scalar forward bound for sigmoid in NF.

sigmoid(x) = 1 / (1 + exp(-x)) is implemented using the existing bounds for exp, +, and division (with the denominator lower-bounded by 1).

noncomputable def Proofs.RuntimeApprox.NFBackend.sigmoidBoundTensor {β : 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 sigmoid.

theorem Proofs.RuntimeApprox.NFBackend.approxT_sigmoid_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 Activation.Math.sigmoidSpec xS) (Spec.Tensor.mapSpec Activation.Math.sigmoidSpec xR) (linfNorm (sigmoidBoundTensor eps xR))

approxT bound for sigmoid lifted to arbitrary tensor shapes.

This is the tensor-level wrapper around sigmoid_bound_scalar (scalar case) and the usual componentwise linf_norm lifting (dimension case).