# 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 definitions #

• real.arsinh: The inverse function of real.sinh.

• real.sinh_equiv, real.sinh_order_iso, real.sinh_homeomorph: real.sinh as an equiv, order_iso, and homeomorph, respectively.

## Main Results #

• real.sinh_surjective, real.sinh_bijective: real.sinh is surjective and bijective;

• real.arsinh_injective, real.arsinh_surjective, real.arsinh_bijective: real.arsinh is injective, surjective, and bijective;

• real.continuous_arsinh, real.differentiable_arsinh, real.cont_diff_arsinh: real.arsinh is continuous, differentiable, and continuously differentiable; we also provide dot notation convenience lemmas like filter.tendsto.arsinh and cont_diff_at.arsinh.

## 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
theorem real.exp_arsinh (x : ) :
= x + real.sqrt (1 + x ^ 2)
@[simp]
theorem real.arsinh_zero  :
= 0
@[simp]
theorem real.arsinh_neg (x : ) :
@[simp]
theorem real.sinh_arsinh (x : ) :
= x

arsinh is the right inverse of sinh.

@[simp]
theorem real.cosh_arsinh (x : ) :
= real.sqrt (1 + x ^ 2)

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

sinh is bijective, both injective and surjective.

@[simp]
theorem real.arsinh_sinh (x : ) :
= x

arsinh is the left inverse of sinh.

@[simp]
theorem real.sinh_equiv_symm_apply (x : ) :
noncomputable def real.sinh_equiv  :

real.sinh as an equiv.

Equations
@[simp]
theorem real.sinh_equiv_apply (x : ) :
@[simp]
@[simp]
noncomputable def real.sinh_order_iso  :

real.sinh as an order_iso.

Equations
@[simp]
@[simp]
noncomputable def real.sinh_homeomorph  :

real.sinh as a homeomorph.

Equations
@[simp]
theorem real.arsinh_inj {x y : } :
x = y
@[simp]
theorem real.arsinh_le_arsinh {x y : } :
x y
@[simp]
theorem real.arsinh_lt_arsinh {x y : } :
x < y
@[simp]
theorem real.arsinh_eq_zero_iff {x : } :
= 0 x = 0
@[simp]
theorem real.arsinh_nonneg_iff {x : } :
0 0 x
@[simp]
theorem real.arsinh_nonpos_iff {x : } :
0 x 0
@[simp]
theorem real.arsinh_pos_iff {x : } :
0 < 0 < x
@[simp]
theorem real.arsinh_neg_iff {x : } :
< 0 x < 0
theorem real.has_deriv_at_arsinh (x : ) :
(real.sqrt (1 + x ^ 2))⁻¹ x
@[continuity]
theorem filter.tendsto.arsinh {α : Type u_1} {l : filter α} {f : α → } {a : } (h : (nhds a)) :
filter.tendsto (λ (x : α), real.arsinh (f x)) l (nhds (real.arsinh a))
theorem continuous_at.arsinh {X : Type u_1} {f : X → } {a : X} (h : a) :
continuous_at (λ (x : X), real.arsinh (f x)) a
theorem continuous_within_at.arsinh {X : Type u_1} {f : X → } {s : set X} {a : X} (h : a) :
continuous_within_at (λ (x : X), real.arsinh (f x)) s a
theorem continuous_on.arsinh {X : Type u_1} {f : X → } {s : set X} (h : s) :
continuous_on (λ (x : X), real.arsinh (f x)) s
theorem continuous.arsinh {X : Type u_1} {f : X → } (h : continuous f) :
continuous (λ (x : X), real.arsinh (f x))
theorem has_strict_fderiv_at.arsinh {E : Type u_1} [ E] {f : E → } {a : E} {f' : E →L[] } (hf : a) :
has_strict_fderiv_at (λ (x : E), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') a
theorem has_fderiv_at.arsinh {E : Type u_1} [ E] {f : E → } {a : E} {f' : E →L[] } (hf : f' a) :
has_fderiv_at (λ (x : E), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') a
theorem has_fderiv_within_at.arsinh {E : Type u_1} [ E] {f : E → } {s : set E} {a : E} {f' : E →L[] } (hf : s a) :
has_fderiv_within_at (λ (x : E), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') s a
theorem differentiable_at.arsinh {E : Type u_1} [ E] {f : E → } {a : E} (h : a) :
(λ (x : E), real.arsinh (f x)) a
theorem differentiable_within_at.arsinh {E : Type u_1} [ E] {f : E → } {s : set E} {a : E} (h : a) :
(λ (x : E), real.arsinh (f x)) s a
theorem differentiable_on.arsinh {E : Type u_1} [ E] {f : E → } {s : set E} (h : s) :
(λ (x : E), real.arsinh (f x)) s
theorem differentiable.arsinh {E : Type u_1} [ E] {f : E → } (h : f) :
(λ (x : E), real.arsinh (f x))
theorem cont_diff_at.arsinh {E : Type u_1} [ E] {f : E → } {a : E} {n : ℕ∞} (h : f a) :
(λ (x : E), real.arsinh (f x)) a
theorem cont_diff_within_at.arsinh {E : Type u_1} [ E] {f : E → } {s : set E} {a : E} {n : ℕ∞} (h : s a) :
(λ (x : E), real.arsinh (f x)) s a
theorem cont_diff.arsinh {E : Type u_1} [ E] {f : E → } {n : ℕ∞} (h : f) :
(λ (x : E), real.arsinh (f x))
theorem cont_diff_on.arsinh {E : Type u_1} [ E] {f : E → } {s : set E} {n : ℕ∞} (h : f s) :
(λ (x : E), real.arsinh (f x)) s
theorem has_strict_deriv_at.arsinh {f : } {a f' : } (hf : a) :
has_strict_deriv_at (λ (x : ), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') a
theorem has_deriv_at.arsinh {f : } {a f' : } (hf : f' a) :
has_deriv_at (λ (x : ), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') a
theorem has_deriv_within_at.arsinh {f : } {s : set } {a f' : } (hf : s a) :
has_deriv_within_at (λ (x : ), real.arsinh (f x)) ((real.sqrt (1 + f a ^ 2))⁻¹ f') s a