TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Interval.InverseHyperbolic

Rational enclosures for inverse hyperbolic functions #

These enclosures compose square roots, logarithms, and exact interval arithmetic. Inverse hyperbolic cosine accepts inputs at least one; inverse hyperbolic tangent requires an interval strictly inside (-1, 1). Inverse hyperbolic sine uses monotonicity and odd symmetry to avoid cancellation in its logarithmic formula at negative inputs. InverseHyperbolicProof proves containment for every real member of an accepted interval.

source
def FloatLib.Numerics.Interval.Internal.asinhFormulaBounds? (I : Interval ℚ) (terms precision : ℕ) :
Option (Interval ℚ)

The logarithmic formula for inverse hyperbolic sine, used at nonnegative endpoints.

Instances For
    source
    def FloatLib.Numerics.Interval.Internal.asinhPointBounds? (x : ℚ) (terms precision : ℕ) :
    Option (Interval ℚ)

    Use odd symmetry before evaluating the logarithmic formula at a negative endpoint.

    Instances For
      source
      def FloatLib.Numerics.Interval.asinhBounds? (I : Interval ℚ) (terms precision : ℕ) :
      Option (Interval ℚ)

      Enclose inverse hyperbolic sine by monotonicity and stable endpoint values.

      Instances For
        source
        def FloatLib.Numerics.Interval.acoshBounds? (I : Interval ℚ) (terms precision : ℕ) :
        Option (Interval ℚ)

        Enclose inverse hyperbolic cosine on intervals with lower endpoint at least one.

        Instances For
          source
          def FloatLib.Numerics.Interval.atanhBounds? (I : Interval ℚ) (terms : ℕ) :
          Option (Interval ℚ)

          Enclose inverse hyperbolic tangent using log ((1 + x) / (1 - x)) / 2. Both poles and intervals reaching them are rejected.

          Instances For