TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Interval.Hyperbolic

Rational intervals for tangent and hyperbolic functions #

Tangent divides the sine enclosure by the cosine enclosure and requires the latter to exclude zero. The hyperbolic functions use exponential enclosures and exact rational arithmetic. Hyperbolic cosine first takes the absolute-value range, retaining its minimum at zero. Hyperbolic tangent uses (exp (2*x) - 1) / (exp (2*x) + 1), whose denominator stays positive.

HyperbolicProof proves containment for every real member of the input interval.

source
def FloatLib.Numerics.Interval.Internal.rationalOutwardRounding :
OutwardRounding ℚ ℚ

Exact rational endpoints need no outward adjustment.

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

    Enclose tangent when the cosine enclosure lies strictly on one side of zero.

    Failure can mean that the input crosses a pole, or that the cosine bounds are too coarse to exclude zero. Increasing the Taylor degree or subdividing the input can resolve the latter.

    Instances For
      source
      def FloatLib.Numerics.Interval.Internal.sinhPointBounds (x : ℚ) (terms : ℕ) :
      Interval ℚ

      Point enclosure from sinh x = (exp x - exp (-x)) / 2.

      Instances For
        source
        def FloatLib.Numerics.Interval.sinhBounds (I : Interval ℚ) (terms : ℕ) :
        Interval ℚ

        Enclose hyperbolic sine by its monotonicity and certified endpoint values.

        Instances For
          source
          def FloatLib.Numerics.Interval.Internal.coshPointBounds (x : ℚ) (terms : ℕ) :
          Interval ℚ

          Point enclosure for hyperbolic cosine, intersected with its range [1, ∞).

          Instances For
            source
            def FloatLib.Numerics.Interval.coshBounds (I : Interval ℚ) (terms : ℕ) :
            Interval ℚ

            Enclose hyperbolic cosine by monotonicity on the absolute-value range.

            An input crossing zero has lower bound one. Both negative and positive intervals retain their endpoint-dependent lower bound; hyperbolic cosine is not monotone on all of the real line.

            Instances For
              source
              def FloatLib.Numerics.Interval.tanhBounds (I : Interval ℚ) (terms : ℕ) :
              Interval ℚ

              Enclose hyperbolic tangent with a positive denominator, even at Taylor degree zero.

              The map (u - 1) / (u + 1) is monotone for u ≥ 0. Clamping the exponential bounds to this domain keeps the result in [-1, 1] without dividing by an enclosure that could contain zero.

              Instances For