mathlib3 documentation

analysis.special_functions.arsinh

Inverse of the sinh function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Main Results #

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

arsinh is the right inverse of sinh.

@[simp]
theorem real.cosh_arsinh (x : ) :

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 : ) :

arsinh is the left inverse of sinh.

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