TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Transcendentals

Opt-in transcendentals for configured binary values #

import FloatLib does not install ExecFloat.Binary.exp, Model.exp, Model.pow, or the MathFunctions instances for configured and model binary values. The class and its host Float and real instances are available without this module. Import this module to give ExecFloat.Binary the deterministic elementary-function kernels (exp, log, sin, cos, sinCos, sinh, cosh, tanh) and the MathFunctions instance. Certified sqrt and abs stay on the default import; this instance only republishes them for generic code.

These functions are deterministic approximations with IEEE-style handling of exceptional inputs. The lifting theorems below say that packing does not change the selected model result; they do not claim a real-error bound or correct rounding. Such claims require a separate certificate or proved enclosure. The optional Arb-backed adapter has its own external-library trust boundary.

The functions use their configured internal approximation and nearest-even arithmetic; they do not accept a per-call rounding direction or return IEEE status flags. Configured.Rounding.Runtime provides directed rounding for the six primitive arithmetic operations, while the Arb adapter is the current explicit-rounding path for transcendental point evaluation.

sinCosResult reports when an argument exceeds the default trigonometric reduction budget. The value-only sin, cos, and sinCos operations return the format's invalid result in that case. This resource failure is separate from IEEE status and from numerical accuracy certificates.

source
@[inline]
def FloatLib.Floats.ExecFloat.Binary.exp {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

Deterministic approximation to eˣ in the configured binary format.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.log {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
    ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

    Deterministic approximation to the natural logarithm in the configured binary format.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Binary.sin {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
      ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

      Deterministic approximation to sine in the configured binary format.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Binary.cos {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
        ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

        Deterministic approximation to cosine in the configured binary format.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.Binary.sinCos {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
          ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) × ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

          Compute sine and cosine together, sharing argument reduction before repacking both results.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.Binary.sinCosResult {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
            Except Formats.BinaryInterchange.Model.Transcendentals.TrigReductionError (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) × ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

            Joint sine/cosine evaluation preserving the model's explicit reduction-budget failure.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.Binary.sinh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
              ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

              Deterministic approximation to hyperbolic sine in the configured binary format.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.ExecFloat.Binary.cosh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                Deterministic approximation to hyperbolic cosine in the configured binary format.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.ExecFloat.Binary.tanh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                  ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                  Deterministic approximation to hyperbolic tangent in the configured binary format.

                  Instances For

                    Representation bridge theorems #

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_exp {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (exp value) = (toModel value).exp

                    Decoding configured exponential exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_log {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (log value) = (toModel value).log

                    Decoding configured logarithm exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_sin {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (sin value) = (toModel value).sin

                    Decoding configured sine exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_cos {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (cos value) = (toModel value).cos

                    Decoding configured cosine exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_sinCos {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    (toModel (sinCos value).1, toModel (sinCos value).2) = (toModel value).sinCos

                    Decoding joint sine/cosine exposes both results of the shared model kernel.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_sinCosResult {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    Except.map (fun (result : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) × ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) => (toModel result.1, toModel result.2)) (sinCosResult value) = (toModel value).sinCosResult

                    Decoding a checked result preserves both the selected values and any reduction-budget error.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_sinh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (sinh value) = (toModel value).sinh

                    Decoding configured hyperbolic sine exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_cosh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (cosh value) = (toModel value).cosh

                    Decoding configured hyperbolic cosine exposes the deterministic model kernel exactly.

                    source
                    @[simp]
                    theorem FloatLib.Floats.ExecFloat.Binary.toModel_tanh {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                    toModel (tanh value) = (toModel value).tanh

                    Decoding configured hyperbolic tangent exposes the deterministic model kernel exactly.

                    source
                    @[instance_reducible]
                    instance FloatLib.Floats.ExecFloat.Binary.instMathFunctionsFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
                    Numerics.MathFunctions (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

                    Configured binary values implement the shared elementary-function interface.

                    This lets generic programs use MathFunctions.exp, MathFunctions.sin, and the other operations without knowing the binary descriptor. sqrt and abs here are the certified operations already on the default import; the remaining fields have the same approximation boundary as the named functions above.