Real semantics of hyperbolic comparisons

Each comparator returns the exact real ordering, including equality at rational special values. The inverse identities are used only on the appropriate real domains.

theorem FloatLib.Numerics.HyperbolicComparison.compareArtanh_eq_real (argument boundary : ℚ) (hlower : -1 < argument) (hupper : argument < 1) : compareArtanh argument boundary hlower hupper = cmp (Real.artanh ↑argument) ↑boundary

Doubling the boundary gives the exact ordering of the inverse hyperbolic tangent.

theorem FloatLib.Numerics.HyperbolicComparison.compareTanh_eq_real (argument boundary : ℚ) : compareTanh argument boundary = cmp (Real.tanh ↑argument) ↑boundary

Inverting the comparison on (-1, 1) gives the exact hyperbolic tangent ordering.

theorem FloatLib.Numerics.HyperbolicComparison.compareSinhPositive_eq_real (argument boundary : ℚ) (hpositive : 0 < argument) : compareSinhPositive argument boundary hpositive = cmp (Real.sinh ↑argument) ↑boundary

The logarithmic preliminary bound and the adaptive hyperbolic sine comparison are both exact.

theorem FloatLib.Numerics.HyperbolicComparison.compareSinh_eq_real (argument boundary : ℚ) : compareSinh argument boundary = cmp (Real.sinh ↑argument) ↑boundary

Odd reflection and the exact zero case preserve the full hyperbolic sine ordering.

theorem FloatLib.Numerics.HyperbolicComparison.compareCoshPositive_eq_real (argument boundary : ℚ) (hpositive : 0 < argument) : compareCoshPositive argument boundary hpositive = cmp (Real.cosh ↑argument) ↑boundary

The logarithmic preliminary bound and the adaptive hyperbolic cosine comparison are both exact.

theorem FloatLib.Numerics.HyperbolicComparison.compareCosh_eq_real (argument boundary : ℚ) : compareCosh argument boundary = cmp (Real.cosh ↑argument) ↑boundary

Even reflection and the exact zero case preserve the full hyperbolic cosine ordering.

theorem FloatLib.Numerics.HyperbolicComparison.compareArsinh_eq_real (argument boundary : ℚ) : compareArsinh argument boundary = cmp (Real.arsinh ↑argument) ↑boundary

Inverse hyperbolic sine comparison agrees with its exact real ordering.

theorem FloatLib.Numerics.HyperbolicComparison.compareArcosh_eq_real (argument boundary : ℚ) (hargument : 1 ≤ argument) : compareArcosh argument boundary = cmp (Real.arcosh ↑argument) ↑boundary

Inverse hyperbolic cosine comparison uses the nonnegative branch on [1, ∞).

theorem FloatLib.Numerics.HyperbolicComparison.prepareArsinhPositive_eq_compare (argument boundary : ℚ) (levels : ℕ) (hpositive : 0 < argument) : (prepareArsinhPositive argument levels hpositive).compare boundary = compareArsinh argument boundary

Cached logarithmic bounds preserve the inverse hyperbolic sine comparator at positive inputs.

theorem FloatLib.Numerics.HyperbolicComparison.prepareArsinh_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareArsinh argument levels).compare boundary = cmp (Real.arsinh ↑argument) ↑boundary

Prepared inverse hyperbolic sine has the same exact real ordering at every boundary.

theorem FloatLib.Numerics.HyperbolicComparison.prepareArcosh_eq_compare (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareArcosh argument levels).compare boundary = compareArcosh argument boundary

Prepared inverse hyperbolic cosine preserves its comparator on all rational inputs.

theorem FloatLib.Numerics.HyperbolicComparison.prepareArcosh_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) (hargument : 1 ≤ argument) : (prepareArcosh argument levels).compare boundary = cmp (Real.arcosh ↑argument) ↑boundary

Prepared inverse hyperbolic cosine agrees with its nonnegative real branch on [1, ∞).

theorem FloatLib.Numerics.HyperbolicComparison.prepareArtanh_eq_real (argument : ℚ) (levels : ℕ) (hlower : -1 < argument) (hupper : argument < 1) (boundary : ℚ) : (prepareArtanh argument levels hlower hupper).compare boundary = cmp (Real.artanh ↑argument) ↑boundary

Caching the fixed logarithm preserves the inverse hyperbolic tangent comparison on (-1, 1).