TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.Calc.Arithmetic

Rounded Arithmetic on Mantissa/Exponent Values #

This module gathers the generic representation-level arithmetic. Addition, subtraction, and multiplication first use their exact NeuralFloat operations. Division and square root need not have finite radix expansions, so they are formed over the reals and rounded directly into the selected format.

These definitions model finite rounded arithmetic. IEEE exceptional behavior for zero divisors, negative square roots, infinities, and NaNs belongs to NN.Floats.IEEEExec.

source
noncomputable def TorchLean.Floats.NeuralFloat.addRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
NeuralFloat β

Exact addition followed by rounding into the selected format.

Instances For
    source
    noncomputable def TorchLean.Floats.NeuralFloat.subRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
    NeuralFloat β

    Exact subtraction followed by rounding into the selected format.

    Instances For
      source
      noncomputable def TorchLean.Floats.NeuralFloat.mulRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
      NeuralFloat β

      Exact multiplication followed by rounding into the selected format.

      Instances For
        source
        noncomputable def TorchLean.Floats.NeuralFloat.divRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
        NeuralFloat β

        Exact real division followed by rounding into the selected format.

        Instances For
          source
          noncomputable def TorchLean.Floats.NeuralFloat.sqrtRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f : NeuralFloat β) :
          NeuralFloat β

          Exact real square root followed by rounding into the selected format.

          Instances For
            source
            @[simp]
            theorem TorchLean.Floats.NeuralFloat.toReal_addRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
            neuralToReal (addRounded rnd f g) = neuralRound rnd (neuralToReal f + neuralToReal g)
            source
            @[simp]
            theorem TorchLean.Floats.NeuralFloat.toReal_subRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
            neuralToReal (subRounded rnd f g) = neuralRound rnd (neuralToReal f - neuralToReal g)
            source
            @[simp]
            theorem TorchLean.Floats.NeuralFloat.toReal_mulRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
            neuralToReal (mulRounded rnd f g) = neuralRound rnd (neuralToReal f * neuralToReal g)
            source
            @[simp]
            theorem TorchLean.Floats.NeuralFloat.toReal_divRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f g : NeuralFloat β) :
            neuralToReal (divRounded rnd f g) = neuralRound rnd (neuralToReal f / neuralToReal g)
            source
            @[simp]
            theorem TorchLean.Floats.NeuralFloat.toReal_sqrtRounded {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (f : NeuralFloat β) :
            neuralToReal (sqrtRounded rnd f) = neuralRound rnd √(neuralToReal f)
            source
            theorem TorchLean.Floats.NeuralFloat.toReal_ne_zero_of_mantissa_ne_zero {β : NeuralRadix} {f : NeuralFloat β} (hf : f.mantissa ≠ 0) :
            neuralToReal f ≠ 0

            A nonzero mantissa gives a nonzero represented real value.

            source
            theorem TorchLean.Floats.NeuralFloat.sq_sqrt_input {β : NeuralRadix} (f : NeuralFloat β) (hf : 0 ≤ neuralToReal f) :
            √(neuralToReal f) ^ 2 = neuralToReal f

            Squaring the exact quantity supplied to sqrtRounded recovers a nonnegative input.