TorchLean API

Docs HomeGuideExamplesGraphs

NN.Proofs.RuntimeApprox.NF.Ops.Elementwise.Core

NF Elementwise Bounds: Core Arithmetic Budgets #

source
noncomputable def Proofs.RuntimeApprox.NFBackend.addBoundTensor {β : 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 addition.

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

Instances For
    source
    noncomputable def Proofs.RuntimeApprox.NFBackend.subBoundTensor {β : 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 subtraction.

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

    Instances For
      source
      noncomputable def Proofs.RuntimeApprox.NFBackend.mulBoundTensor {β : 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 multiplication.

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

      Instances For
        source
        noncomputable def Proofs.RuntimeApprox.NFBackend.scaleBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (c : TorchLean.Floats.NF β fexp rnd) (xR : Spec.Tensor (TorchLean.Floats.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).

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

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

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

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

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

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

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

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

                  Instances For
                    source
                    theorem Proofs.RuntimeApprox.NFBackend.approxT_safeLog_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} (ε : ℝ) (hε : 0 < ε) {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} :
                    approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec (safeLog ε) xS) (Spec.Tensor.mapSpec (safeLogR ε) xR) (linfNorm (safeLogBoundTensor ε eps xR))

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

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