Inverse hyperbolic functions

Definition

The inverse hyperbolic sine $\operatorname{arsinh} \colon \mathbb{R} \to \mathbb{R}$ is the inverse of $\sinh$. The inverse hyperbolic cosine $\operatorname{arcosh} \colon [1, \infty) \to [0, \infty)$ is the inverse of the restriction of $\cosh$ to $[0, \infty)$. The inverse hyperbolic tangent $\operatorname{artanh} \colon (-1, 1) \to \mathbb{R}$ is the inverse of $\tanh$.

Remarks

Solving a quadratic equation in $e^y$ gives the formulas $\operatorname{arsinh} x = \ln(x + \sqrt{x^2 + 1})$ and $\operatorname{arcosh} x = \ln(x + \sqrt{x^2 - 1})$. Similarly, $\operatorname{artanh} x = \frac{1}{2} \ln \frac{1 + x}{1 - x}$ for $|x| < 1$. Their derivatives are $\frac{1}{\sqrt{x^2 + 1}}$, $\frac{1}{\sqrt{x^2 - 1}}$ for $x > 1$, and $\frac{1}{1 - x^2}$. Mathlib defines the first one as Real.arsinh.

Explanations

L1 human

The inverse hyperbolic functions undo the hyperbolic functions. Since the hyperbolic functions come from $e^x$, their inverses come from the logarithm.