mathlibdocumentation

analysis.special_functions.arsinh

Inverse of the sinh function #

In this file we prove that sinh is bijective and hence has an inverse, arsinh.

Main Results #

• sinh_injective: The proof that sinh is injective
• sinh_surjective: The proof that sinh is surjective
• sinh_bijective: The proof sinh is bijective
• arsinh: The inverse function of sinh

Tags #

arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective

noncomputable def real.arsinh (x : ) :

arsinh is defined using a logarithm, arsinh x = log (x + sqrt(1 + x^2)).

Equations

sinh is injective, ∀ a b, sinh a = sinh b → a = b.

theorem real.sinh_arsinh (x : ) :
= x

arsinh is the right inverse of sinh.

sinh is surjective, ∀ b, ∃ a, sinh a = b. In this case, we use a = arsinh b.

sinh is bijective, both injective and surjective.

theorem real.sqrt_one_add_sinh_sq (x : ) :
real.sqrt (1 + ^ 2) =

A rearrangement and sqrt of real.cosh_sq_sub_sinh_sq.

theorem real.arsinh_sinh (x : ) :
= x

arsinh is the left inverse of sinh.