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

noncomputable def Real.arsinh (x : ℝ) : ℝ

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

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

@[simp]

theorem Real.arsinh_zero : arsinh 0 = 0

@[simp]

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

@[simp]

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

arsinh is the right inverse of sinh.

@[simp]

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

@[simp]

theorem Real.tanh_arsinh (x : ℝ) : tanh (arsinh x) = x / √(1 + x ^ 2)

theorem Real.sinh_surjective : Function.Surjective sinh

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

theorem Real.sinh_bijective : Function.Bijective sinh

sinh is bijective, both injective and surjective.

@[simp]

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

arsinh is the left inverse of sinh.

noncomputable def Real.sinhEquiv : ℝ ≃ ℝ

Real.sinh as an Equiv.

@[simp]

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

@[simp]

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

noncomputable def Real.sinhOrderIso : ℝ ≃o ℝ

Real.sinh as an OrderIso.

@[simp]

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

@[simp]

theorem Real.sinhOrderIso_apply : ⇑sinhOrderIso = sinh

noncomputable def Real.sinhHomeomorph : ℝ ≃ₜ ℝ

Real.sinh as a Homeomorph.

@[simp]

theorem Real.sinhHomeomorph_apply : ⇑sinhHomeomorph = sinh

@[simp]

theorem Real.sinhHomeomorph_symm_apply : ⇑sinhHomeomorph.symm = EquivLike.inv sinhOrderIso

theorem Real.arsinh_bijective : Function.Bijective arsinh

theorem Real.arsinh_injective : Function.Injective arsinh

theorem Real.arsinh_surjective : Function.Surjective arsinh

theorem Real.arsinh_strictMono : StrictMono arsinh

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.arsinh_pos_iff {x : ℝ} : 0 < arsinh x ↔ 0 < x

@[simp]

theorem Real.arsinh_neg_iff {x : ℝ} : arsinh x < 0 ↔ x < 0

theorem Real.hasStrictDerivAt_arsinh (x : ℝ) : HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x

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

theorem Real.differentiable_arsinh : Differentiable ℝ arsinh

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

theorem Real.continuous_arsinh : Continuous arsinh

theorem Real.analyticAt_arsinh {x : ℝ} : AnalyticAt ℝ arsinh x

The function Real.arsinh is real analytic.

theorem Real.analyticWithinAt_arsinh {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ arsinh s x

The function Real.arsinh is real analytic.

theorem Real.analyticOnNhd_arsinh {s : Set ℝ} : AnalyticOnNhd ℝ arsinh s

The function Real.arsinh is real analytic.

theorem Real.analyticOn_arsinh {s : Set ℝ} : AnalyticOn ℝ arsinh s

The function Real.arsinh is real analytic.

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

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

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

theorem HasFDerivAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : StrongDual ℝ E} (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} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E} {f' : StrongDual ℝ E} (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} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} (h : DifferentiableAt ℝ f a) : DifferentiableAt ℝ (fun (x : E) => 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 : E) => 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 : E) => Real.arsinh (f x)) s

theorem Differentiable.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (h : Differentiable ℝ f) : Differentiable ℝ fun (x : E) => 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 : E) => 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 : E) => 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 : E) => 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 : 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 : Set ℝ} {a f' : ℝ} (hf : HasDerivWithinAt f f' s a) : HasDerivWithinAt (fun (x : ℝ) => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') s a