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

theorem Real.exp_arsinh (x : ℝ) : Real.exp (Real.arsinh x) = x + Real.sqrt (1 + x ^ 2)

@[simp]

theorem Real.arsinh_zero : Real.arsinh 0 = 0

@[simp]

theorem Real.arsinh_neg (x : ℝ) : Real.arsinh (-x) = -Real.arsinh x

@[simp]

theorem Real.sinh_arsinh (x : ℝ) : Real.sinh (Real.arsinh x) = x

arsinh is the right inverse of sinh.

@[simp]

theorem Real.cosh_arsinh (x : ℝ) : Real.cosh (Real.arsinh x) = Real.sqrt (1 + x ^ 2)

theorem Real.sinh_surjective : Function.Surjective Real.sinh

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

theorem Real.sinh_bijective : Function.Bijective Real.sinh

sinh is bijective, both injective and surjective.

@[simp]

theorem Real.arsinh_sinh (x : ℝ) : Real.arsinh (Real.sinh x) = x

arsinh is the left inverse of sinh.

@[simp]

theorem Real.sinhEquiv_symm_apply (x : ℝ) : ↑Real.sinhEquiv.symm x = Real.arsinh x

@[simp]

theorem Real.sinhEquiv_apply (x : ℝ) : ↑Real.sinhEquiv x = Real.sinh x

def Real.sinhEquiv : ℝ ≃ ℝ

Real.sinh as an Equiv.

@[simp]

theorem Real.sinhOrderIso_symm_apply : ↑(RelIso.symm Real.sinhOrderIso) = Real.arsinh

@[simp]

theorem Real.sinhOrderIso_apply : ↑Real.sinhOrderIso = Real.sinh

def Real.sinhOrderIso : ℝ ≃o ℝ

Real.sinh as an OrderIso.

@[simp]

theorem Real.sinhHomeomorph_symm_apply : ↑(Homeomorph.symm Real.sinhHomeomorph) = Real.arsinh

@[simp]

theorem Real.sinhHomeomorph_apply : ↑Real.sinhHomeomorph = Real.sinh

def Real.sinhHomeomorph : ℝ ≃ₜ ℝ

Real.sinh as a Homeomorph.

theorem Real.arsinh_bijective : Function.Bijective Real.arsinh

theorem Real.arsinh_injective : Function.Injective Real.arsinh

theorem Real.arsinh_surjective : Function.Surjective Real.arsinh

theorem Real.arsinh_strictMono : StrictMono Real.arsinh

@[simp]

theorem Real.arsinh_inj {x : ℝ} {y : ℝ} : Real.arsinh x = Real.arsinh y ↔ x = y

@[simp]

theorem Real.arsinh_le_arsinh {x : ℝ} {y : ℝ} : Real.arsinh x ≤ Real.arsinh y ↔ x ≤ y

@[simp]

theorem Real.arsinh_lt_arsinh {x : ℝ} {y : ℝ} : Real.arsinh x < Real.arsinh y ↔ x < y

@[simp]

theorem Real.arsinh_eq_zero_iff {x : ℝ} : Real.arsinh x = 0 ↔ x = 0

@[simp]

theorem Real.arsinh_nonneg_iff {x : ℝ} : 0 ≤ Real.arsinh x ↔ 0 ≤ x

@[simp]

theorem Real.arsinh_nonpos_iff {x : ℝ} : Real.arsinh x ≤ 0 ↔ x ≤ 0

@[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 Real.hasStrictDerivAt_arsinh (x : ℝ) : HasStrictDerivAt Real.arsinh (Real.sqrt (1 + x ^ 2))⁻¹ x

theorem Real.hasDerivAt_arsinh (x : ℝ) : HasDerivAt Real.arsinh (Real.sqrt (1 + x ^ 2))⁻¹ x

theorem Real.differentiable_arsinh : Differentiable ℝ Real.arsinh

theorem Real.contDiff_arsinh {n : ℕ∞} : ContDiff ℝ n Real.arsinh

theorem Real.continuous_arsinh : Continuous Real.arsinh

theorem Filter.Tendsto.arsinh {α : Type u_1} {l : Filter α} {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} [TopologicalSpace X] {f : X → ℝ} {a : X} (h : ContinuousAt f a) : ContinuousAt (fun x => Real.arsinh (f x)) a

theorem ContinuousWithinAt.arsinh {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} {a : X} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => Real.arsinh (f x)) s a

theorem ContinuousOn.arsinh {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun x => Real.arsinh (f x)) s

theorem Continuous.arsinh {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} (h : Continuous f) : Continuous fun x => Real.arsinh (f x)

theorem HasStrictFDerivAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ} (hf : HasStrictFDerivAt f f' a) : HasStrictFDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') a

theorem HasFDerivAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' a) : HasFDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') a

theorem HasFDerivWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E} {f' : E →L[ℝ] ℝ} (hf : HasFDerivWithinAt f f' s a) : HasFDerivWithinAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') s a

theorem DifferentiableAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} (h : DifferentiableAt ℝ f a) : DifferentiableAt ℝ (fun x => Real.arsinh (f x)) a

theorem DifferentiableWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E} (h : DifferentiableWithinAt ℝ f s a) : DifferentiableWithinAt ℝ (fun x => Real.arsinh (f x)) s a

theorem DifferentiableOn.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (h : DifferentiableOn ℝ f s) : DifferentiableOn ℝ (fun x => Real.arsinh (f x)) s

theorem Differentiable.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (h : Differentiable ℝ f) : Differentiable ℝ fun x => Real.arsinh (f x)

theorem ContDiffAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} {n : ℕ∞} (h : ContDiffAt ℝ n f a) : ContDiffAt ℝ n (fun x => Real.arsinh (f x)) a

theorem ContDiffWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E} {n : ℕ∞} (h : ContDiffWithinAt ℝ n f s a) : ContDiffWithinAt ℝ n (fun x => Real.arsinh (f x)) s a

theorem ContDiff.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ n f) : ContDiff ℝ n fun x => Real.arsinh (f x)

theorem ContDiffOn.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞} (h : ContDiffOn ℝ n f s) : ContDiffOn ℝ n (fun x => Real.arsinh (f x)) s

theorem HasStrictDerivAt.arsinh {f : ℝ → ℝ} {a : ℝ} {f' : ℝ} (hf : HasStrictDerivAt f f' a) : HasStrictDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') a

theorem HasDerivAt.arsinh {f : ℝ → ℝ} {a : ℝ} {f' : ℝ} (hf : HasDerivAt f f' a) : HasDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') a

theorem HasDerivWithinAt.arsinh {f : ℝ → ℝ} {s : Set ℝ} {a : ℝ} {f' : ℝ} (hf : HasDerivWithinAt f f' s a) : HasDerivWithinAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ • f') s a