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 #

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

source

noncomputable def real.arsinh (x : ℝ) :

ℝ

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

Equations

real.arsinh x = real.log (x + √ (1 + x ^ 2))

source

theorem real.exp_arsinh (x : ℝ) :

rexp (real.arsinh x) = x + √ (1 + x ^ 2)

source

@[simp]

theorem real.arsinh_zero :

real.arsinh 0 = 0

source

@[simp]

theorem real.arsinh_neg (x : ℝ) :

real.arsinh (-x) = -real.arsinh x

source

@[simp]

theorem real.sinh_arsinh (x : ℝ) :

real.sinh (real.arsinh x) = x

arsinh is the right inverse of sinh.

source

@[simp]

theorem real.cosh_arsinh (x : ℝ) :

real.cosh (real.arsinh x) = √ (1 + x ^ 2)

source

theorem real.sinh_surjective :

function.surjective real.sinh

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

source

theorem real.sinh_bijective :

function.bijective real.sinh

sinh is bijective, both injective and surjective.

source

@[simp]

theorem real.arsinh_sinh (x : ℝ) :

real.arsinh (real.sinh x) = x

arsinh is the left inverse of sinh.

source

@[simp]

theorem real.sinh_equiv_symm_apply (x : ℝ) :

⇑(real.sinh_equiv.symm) x = real.arsinh x

source

noncomputable def real.sinh_equiv :

ℝ ≃ ℝ

real.sinh as an equiv.

Equations

real.sinh_equiv = {to_fun := real.sinh, inv_fun := real.arsinh, left_inv := real.arsinh_sinh, right_inv := real.sinh_arsinh}

source

@[simp]

theorem real.sinh_equiv_apply (x : ℝ) :

⇑real.sinh_equiv x = real.sinh x

source

@[simp]

theorem real.sinh_order_iso_symm_apply :

⇑(rel_iso.symm real.sinh_order_iso) = real.arsinh

source

@[simp]

theorem real.sinh_order_iso_apply :

⇑real.sinh_order_iso = real.sinh

source

noncomputable def real.sinh_order_iso :

ℝ ≃o ℝ

real.sinh as an order_iso.

Equations

real.sinh_order_iso = {to_equiv := real.sinh_equiv, map_rel_iff' := real.sinh_le_sinh}

source

@[simp]

theorem real.sinh_homeomorph_apply :

⇑real.sinh_homeomorph = real.sinh

source

@[simp]

theorem real.sinh_homeomorph_symm_apply :

⇑(real.sinh_homeomorph.symm) = real.arsinh

source

noncomputable def real.sinh_homeomorph :

ℝ ≃ₜ ℝ

real.sinh as a homeomorph.

Equations

real.sinh_homeomorph = real.sinh_order_iso.to_homeomorph

source

theorem real.arsinh_bijective :

function.bijective real.arsinh

source

theorem real.arsinh_injective :

function.injective real.arsinh

source

theorem real.arsinh_surjective :

function.surjective real.arsinh

source

theorem real.arsinh_strict_mono :

strict_mono real.arsinh

source

@[simp]

theorem real.arsinh_inj {x y : ℝ} :

real.arsinh x = real.arsinh y ↔ x = y

source

@[simp]

theorem real.arsinh_le_arsinh {x y : ℝ} :

real.arsinh x ≤ real.arsinh y ↔ x ≤ y

source

@[simp]

theorem real.arsinh_lt_arsinh {x y : ℝ} :

real.arsinh x < real.arsinh y ↔ x < y

source

@[simp]

theorem real.arsinh_eq_zero_iff {x : ℝ} :

real.arsinh x = 0 ↔ x = 0

source

@[simp]

theorem real.arsinh_nonneg_iff {x : ℝ} :

0 ≤ real.arsinh x ↔ 0 ≤ x

source

@[simp]

theorem real.arsinh_nonpos_iff {x : ℝ} :

real.arsinh x ≤ 0 ↔ x ≤ 0

source

@[simp]

theorem real.arsinh_pos_iff {x : ℝ} :

0 < real.arsinh x ↔ 0 < x

source

@[simp]

theorem real.arsinh_neg_iff {x : ℝ} :

real.arsinh x < 0 ↔ x < 0

source

theorem real.has_strict_deriv_at_arsinh (x : ℝ) :

has_strict_deriv_at real.arsinh (√ (1 + x ^ 2))⁻¹ x

source

theorem real.has_deriv_at_arsinh (x : ℝ) :

has_deriv_at real.arsinh (√ (1 + x ^ 2))⁻¹ x

source

theorem real.differentiable_arsinh :

differentiable ℝ real.arsinh

source

theorem real.cont_diff_arsinh {n : ℕ∞} :

cont_diff ℝ n real.arsinh

source

@[continuity]

theorem real.continuous_arsinh :

continuous real.arsinh

source

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

source

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

source

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

source

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

source

theorem continuous.arsinh {X : Type u_1} [topological_space X] {f : X → ℝ} (h : continuous f) :

continuous (λ (x : X), real.arsinh (f x))

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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