# 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.sinhEquiv, Real.sinhOrderIso, Real.sinhHomeomorph: Real.sinh as an Equiv, OrderIso, 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.contDiff_arsinh: Real.arsinh is continuous, differentiable, and continuously differentiable; we also provide dot notation convenience lemmas like Filter.Tendsto.arsinh and ContDiffAt.arsinh.

## Tags #

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

def Real.arsinh (x : ) :

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

Equations
Instances For
theorem Real.exp_arsinh (x : ) :
= x + (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 : ) :
= (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.sinhEquiv_apply (x : ) :
Real.sinhEquiv x =
@[simp]

Real.sinh as an Equiv.

Equations
Instances For
@[simp]
@[simp]

Real.sinh as an OrderIso.

Equations
Instances For
@[simp]

Real.sinh as a Homeomorph.

Equations
Instances For
@[simp]
theorem Real.arsinh_inj {x : } {y : } :
x = y
@[simp]
theorem Real.arsinh_le_arsinh {x : } {y : } :
x y
theorem Real.GCongr.arsinh_le_arsinh {x : } {y : } :
x y

Alias of the reverse direction of Real.arsinh_le_arsinh.

@[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 Filter.Tendsto.arsinh {α : Type u_1} {l : } {f : α} {a : } (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (x : α) => Real.arsinh (f x)) l (nhds (Real.arsinh a))
theorem ContinuousAt.arsinh {X : Type u_1} [] {f : X} {a : X} (h : ) :
ContinuousAt (fun (x : X) => Real.arsinh (f x)) a
theorem ContinuousWithinAt.arsinh {X : Type u_1} [] {f : X} {s : Set X} {a : X} (h : ) :
ContinuousWithinAt (fun (x : X) => Real.arsinh (f x)) s a
theorem ContinuousOn.arsinh {X : Type u_1} [] {f : X} {s : Set X} (h : ) :
ContinuousOn (fun (x : X) => Real.arsinh (f x)) s
theorem Continuous.arsinh {X : Type u_1} [] {f : X} (h : ) :
Continuous fun (x : X) => Real.arsinh (f x)
theorem HasStrictFDerivAt.arsinh {E : Type u_1} [] {f : E} {a : E} {f' : } (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') a
theorem HasFDerivAt.arsinh {E : Type u_1} [] {f : E} {a : E} {f' : } (hf : HasFDerivAt f f' a) :
HasFDerivAt (fun (x : E) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') a
theorem HasFDerivWithinAt.arsinh {E : Type u_1} [] {f : E} {s : Set E} {a : E} {f' : } (hf : HasFDerivWithinAt f f' s a) :
HasFDerivWithinAt (fun (x : E) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') s a
theorem DifferentiableAt.arsinh {E : Type u_1} [] {f : E} {a : E} (h : ) :
DifferentiableAt (fun (x : E) => Real.arsinh (f x)) a
theorem DifferentiableWithinAt.arsinh {E : Type u_1} [] {f : E} {s : Set E} {a : E} (h : ) :
DifferentiableWithinAt (fun (x : E) => Real.arsinh (f x)) s a
theorem DifferentiableOn.arsinh {E : Type u_1} [] {f : E} {s : Set E} (h : ) :
DifferentiableOn (fun (x : E) => Real.arsinh (f x)) s
theorem Differentiable.arsinh {E : Type u_1} [] {f : E} (h : ) :
Differentiable fun (x : E) => Real.arsinh (f x)
theorem ContDiffAt.arsinh {E : Type u_1} [] {f : E} {a : E} {n : ℕ∞} (h : ContDiffAt n f a) :
ContDiffAt n (fun (x : E) => Real.arsinh (f x)) a
theorem ContDiffWithinAt.arsinh {E : Type u_1} [] {f : E} {s : Set E} {a : E} {n : ℕ∞} (h : ) :
ContDiffWithinAt n (fun (x : E) => Real.arsinh (f x)) s a
theorem ContDiff.arsinh {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.arsinh (f x)
theorem ContDiffOn.arsinh {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (h : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.arsinh (f x)) s
theorem HasStrictDerivAt.arsinh {f : } {a : } {f' : } (hf : HasStrictDerivAt f f' a) :
HasStrictDerivAt (fun (x : ) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') a
theorem HasDerivAt.arsinh {f : } {a : } {f' : } (hf : HasDerivAt f f' a) :
HasDerivAt (fun (x : ) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') a
theorem HasDerivWithinAt.arsinh {f : } {s : } {a : } {f' : } (hf : HasDerivWithinAt f f' s a) :
HasDerivWithinAt (fun (x : ) => Real.arsinh (f x)) (((1 + f a ^ 2))⁻¹ f') s a