Exact comparisons for hyperbolic functions

Inverse hyperbolic tangent reduces to a logarithm of an exact rational ratio. Hyperbolic tangent uses the same comparison in reverse. Neither operation constructs an exponential at the input, so large rational arguments do not produce exponentially large integers.

Hyperbolic sine and cosine first compare the exponential with a rational bound using a logarithm. Only unresolved cases construct exponential enclosures; in those cases the exponential lies in a rational interval of width one around twice the comparison boundary.

def FloatLib.Numerics.HyperbolicComparison.compareArtanh (argument boundary : ℚ) (hlower : -1 < argument) (hupper : argument < 1) : Ordering

Compare artanh argument with a rational boundary on its open real domain.

def FloatLib.Numerics.HyperbolicComparison.compareTanh (argument boundary : ℚ) : Ordering

Compare hyperbolic tangent with a rational boundary, using its inverse on (-1, 1).

def FloatLib.Numerics.HyperbolicComparison.compareSinhPositive (argument boundary : ℚ) (hpositive : 0 < argument) : Ordering

Compare positive-argument hyperbolic sine using the bounds 0 < exp (-x) < 1. Only 2 * boundary < exp x < 2 * boundary + 1 requires exponential enclosures.

def FloatLib.Numerics.HyperbolicComparison.compareSinh (argument boundary : ℚ) : Ordering

Exact hyperbolic sine comparison, using odd symmetry for negative inputs.

def FloatLib.Numerics.HyperbolicComparison.compareCoshPositive (argument boundary : ℚ) (hpositive : 0 < argument) : Ordering

Compare positive-argument hyperbolic cosine using the bounds 0 < exp (-x) < 1. Only 2 * boundary - 1 < exp x < 2 * boundary requires exponential enclosures.

def FloatLib.Numerics.HyperbolicComparison.compareCosh (argument boundary : ℚ) : Ordering

Exact hyperbolic cosine comparison, using even symmetry and handling zero exactly.

def FloatLib.Numerics.HyperbolicComparison.compareArsinh (argument boundary : ℚ) : Ordering

Compare inverse hyperbolic sine by the globally increasing hyperbolic sine.

def FloatLib.Numerics.HyperbolicComparison.compareArcosh (argument boundary : ℚ) : Ordering

Compare inverse hyperbolic cosine on its nonnegative branch; callers require argument ≥ 1.

def FloatLib.Numerics.HyperbolicComparison.prepareArsinhPositive (argument : ℚ) (levels : ℕ) (hpositive : 0 < argument) : Enclosure.Comparison.Prepared

Prepare inverse hyperbolic sine at a positive argument.

The two logarithmic bounds depend only on the argument. Their enclosure caches are allocated before the boundary closure, so rounding queries share the first levels Taylor enclosures.

def FloatLib.Numerics.HyperbolicComparison.prepareArsinh (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare inverse hyperbolic sine, sharing logarithmic bounds and using odd symmetry.

def FloatLib.Numerics.HyperbolicComparison.prepareArcosh (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare inverse hyperbolic cosine with shared logarithms of 2 * argument and 2 * argument - 1. The real-domain contract remains argument ≥ 1.

def FloatLib.Numerics.HyperbolicComparison.prepareArtanh (argument : ℚ) (levels : ℕ) (hlower : -1 < argument) (hupper : argument < 1) : Enclosure.Comparison.Prepared

Prepare inverse hyperbolic tangent, sharing the logarithm of its exact rational ratio.