Containment for inverse hyperbolic functions

Each successful enclosure follows the corresponding real logarithmic identity. Domain checks for inverse hyperbolic cosine and tangent apply to every real member of the input interval.

theorem FloatLib.Numerics.Interval.containsReal_asinhBounds? {I K : Interval ℚ} {terms precision : ℕ} (h : I.asinhBounds? terms precision = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.arsinh x)

Successful inverse hyperbolic sine bounds contain the image of every enclosed real value.

theorem FloatLib.Numerics.Interval.containsReal_acoshBounds? {I K : Interval ℚ} {terms precision : ℕ} (h : I.acoshBounds? terms precision = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.arcosh x)

Successful inverse hyperbolic cosine bounds contain the image of every enclosed real value.

theorem FloatLib.Numerics.Interval.containsReal_atanhBounds? {I K : Interval ℚ} {terms : ℕ} (h : I.atanhBounds? terms = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.artanh x)

Successful inverse hyperbolic tangent bounds contain the image of every enclosed real value.