NF Elementwise Bounds: Core Arithmetic Budgets

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

Per-entry bound tensor for addition.

add_bound_tensor epsx epsy xR yR computes an elementwise error budget for xR + yR. Its linfNorm is used as the output epsilon in approxTensor_add_spec.

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

Per-entry bound tensor for subtraction.

Analogous to addBoundTensor, but for xR - yR (and the corresponding spec subtraction).

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

Per-entry bound tensor for multiplication.

This is the elementwise lifting of the scalar bound approx_mul_nf, tracking first-order error propagation plus one rounding term.

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

Per-entry bound tensor for scaling by a runtime constant.

scale_bound_tensor eps c xR bounds the error of xR * c assuming the input is approximated within eps and treating c as exact (relative to its own toSpec value).

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

Per-entry budget for scaling when the scalar coefficient is itself approximate.

scaleBoundTensor is the zero-coefficient-error specialization. This general form is required by constants such as 1 / sqrt(d) in attention, where constructing the runtime coefficient already incurs rounding.

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

noncomputable def Proofs.RuntimeApprox.NFBackend.absBoundTensor {β : 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 absolute value.

noncomputable def Proofs.RuntimeApprox.NFBackend.expBoundTensor {β : 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 exponentiation (exp).

This matches approx_exp_nf: a mean-value-theorem bound on the real exp plus one rounding term.

noncomputable def Proofs.RuntimeApprox.NFBackend.sqrtPosBoundTensor {β : 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 square-root budget on a domain with exact lower bound η.

noncomputable def Proofs.RuntimeApprox.NFBackend.tanhBoundTensor {β : 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 hyperbolic tangent (tanh).

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

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

safeLog_bound_tensor ε eps xR is the elementwise bound used by approxTensor_safeLog_spec, combining a (1/ε) Lipschitz propagation term with one rounding-ULP term.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_safeLog_spec {β : 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 → approxTensor toSpec (TorchLean.Tensor.mapSpec (safeLog ε) xS) (TorchLean.Tensor.mapSpec (safeLogR ε) xR) (linfNorm (safeLogBoundTensor ε eps xR))

approxTensor bound for clamped log (safeLog) lifted to arbitrary tensor shapes.

This is the tensor-level wrapper around approx_safeLog_nf, using approxTensor_map_spec_of_scalar_bound.