[Merged by Bors] - feat(analysis/special_functions/arsinh): inverse hyperbolic sine function

src/analysis/special_functions/arsinh.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2020 James Arthur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: James Arthur, Chris Hughes, Shing Tak Lam
+-/
+import analysis.special_functions.trigonometric
+
+open real
+noncomputable theory
+
+/-!
+# Inverse of the sinh function
+
+In this file we prove that sinh is bijective and hence has an
+inverse, arsinh.
+
+## Main Results
+
+- `sinh_injective`: The proof that `sinh` is injective
+- `sinh_surjective`: The proof that `sinh` is surjective
+- `sinh_bijective`: The proof `sinh` is bijective
+- `arsinh`: The inverse function of `sinh`
+
+## Tags
+
+arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective
+-/
+
+
+/-- `arsinh` is defined using a logarithm, `arsinh x = log (x + sqrt(1 + x^2))` -/
+def arsinh (x : ℝ) := log (x + sqrt (1 + x^2))
+
+/-- `sinh` is injective, `∀ a b, sinh a = sinh b → a = b` -/
+lemma sinh_injective : function.injective sinh := sinh_strict_mono.injective
+
+private lemma aux_lemma (x : ℝ) : 1 / (x + sqrt (1 + x ^ 2)) = -x + sqrt (1 + x ^ 2) :=
+begin
+  refine (eq_one_div_of_mul_eq_one _).symm,
+  have : 0 ≤ 1 + x ^ 2 := add_nonneg zero_le_one (pow_two_nonneg x),
+  rw [add_comm, ← sub_eq_neg_add, ← mul_self_sub_mul_self,
+      mul_self_sqrt this, pow_two, add_sub_cancel]
+end
+
+private lemma b_lt_sqrt_b_one_add_sq (b : ℝ) : b < sqrt (1 + b ^ 2) :=
+calc  b
+    ≤ sqrt (b ^ 2)     : le_sqrt_of_sqr_le $ le_refl _
+... < sqrt (1 + b ^ 2) : (sqrt_lt (pow_two_nonneg _) (add_nonneg zero_le_one (pow_two_nonneg _))).2
+  (lt_one_add _)
+
+private lemma add_sqrt_one_add_pow_two_pos (b : ℝ) : 0 < b + sqrt (1 + b ^ 2) :=
+by { rw [← neg_neg b, ← sub_eq_neg_add, sub_pos, pow_two, neg_mul_neg, ← pow_two],
+  exact b_lt_sqrt_b_one_add_sq (-b) }
+
+/-- `arsinh` is the right inverse of `sinh`-/
+lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x :=
+by rw [sinh_eq, arsinh, ← log_inv, exp_log (add_sqrt_one_add_pow_two_pos x),
+      exp_log (inv_pos.2 (add_sqrt_one_add_pow_two_pos x)),
+      inv_eq_one_div, aux_lemma x, sub_eq_add_neg, neg_add, neg_neg, ← sub_eq_add_neg,
+      add_add_sub_cancel, add_self_div_two]
+
+/-- `sinh` is surjective, `∀ b, ∃ a, sinh a = b`. In this case, we use `a = arsinh b` -/
+lemma sinh_surjective : function.surjective sinh := function.left_inverse.surjective arsinh_sinh
+
+/-- `sinh` is bijective, both injective and surjective. -/
+lemma sinh_bijective : function.bijective sinh :=
+⟨sinh_injective, sinh_surjective⟩
+
+/-- A rearrangment and `sqrt` of `real.cosh_sq_sub_sinh_sq` -/
+lemma sqrt_one_add_sinh_sq (x : ℝ): sqrt (1 + sinh x ^ 2) = cosh x :=
+begin
+  have H := real.cosh_sq_sub_sinh_sq x,
+  have G : cosh x ^ 2 - sinh x ^ 2 + sinh x ^ 2 = 1 + sinh x ^ 2 := by rw H,
+  rw sub_add_cancel at G,
+  rw [←G, sqrt_sqr],
+  exact le_of_lt (cosh_pos x),
+end
+
+/-- `arsinh` is the left inverse of `sinh` -/
+lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x :=
+function.right_inverse_of_injective_of_left_inverse sinh_injective arsinh_sinh x

src/analysis/special_functions/exp_log.lean

@@ -198,7 +198,7 @@ end
 to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
 `(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
 the derivative of `log` is `1/x` away from `0`. -/
-noncomputable def log (x : ℝ) : ℝ :=
+@[pp_nodot] noncomputable def log (x : ℝ) : ℝ :=
 if hx : x ≠ 0 then classical.some (exists_exp_eq_of_pos (abs_pos_iff.mpr hx)) else 0
 
 lemma exp_log_eq_abs (hx : x ≠ 0) : exp (log x) = abs x :=

src/analysis/special_functions/trigonometric.lean

@@ -348,6 +348,10 @@ funext $ λ x, (has_deriv_at_cosh x).deriv
 lemma continuous_cosh : continuous cosh :=
 differentiable_cosh.continuous
 
+/-- `sinh` is strictly monotone. -/
+lemma sinh_strict_mono : strict_mono sinh :=
+strict_mono_of_deriv_pos differentiable_sinh (by { rw [real.deriv_sinh], exact cosh_pos })
+
 end real
 
 section

src/data/complex/exponential.lean

@@ -862,6 +862,11 @@ of_real_inj.1 $ by simpa using cos_square x
 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
 eq_sub_iff_add_eq.2 $ sin_sq_add_cos_sq _
 
+/-- The definition of `sinh` in terms of `exp` -/
+lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 :=
+eq_div_of_mul_eq two_ne_zero $ by rw [sinh, exp, exp, complex.of_real_neg, complex.sinh, mul_two,
+    ← complex.add_re, ← mul_two, div_mul_cancel _ (two_ne_zero' : (2 : ℂ) ≠ 0), complex.sub_re]
+
 @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
 
 @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
@@ -870,6 +875,11 @@ by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]
 lemma sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y :=
 by rw ← of_real_inj; simp [sinh_add]
 
+/-- The definition of `cosh` in terms of `exp`. -/
+lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 :=
+eq_div_of_mul_eq two_ne_zero $ by rw [cosh, exp, exp, complex.of_real_neg, complex.cosh, mul_two,
+    ← complex.add_re, ← mul_two, div_mul_cancel _ (two_ne_zero' : (2 : ℂ) ≠ 0), complex.add_re]
+
 @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh]
 
 @[simp] lemma cosh_neg : cosh (-x) = cosh x :=
@@ -884,6 +894,16 @@ by simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]
 lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
 by simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]
 
+lemma cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 :=
+begin
+  rw [sinh, cosh],
+  have := congr_arg complex.re (complex.cosh_sq_sub_sinh_sq x),
+  rw [pow_two, pow_two] at this,
+  change (⟨_, _⟩ : ℂ).re - (⟨_, _⟩ : ℂ).re = 1 at this,
+  rw [complex.cosh_of_real_im x, complex.sinh_of_real_im x, mul_zero, sub_zero, sub_zero] at this,
+  rwa [pow_two, pow_two],
+end
+
 lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
 of_real_inj.1 $ by simp [tanh_eq_sinh_div_cosh]
 
@@ -944,6 +964,10 @@ by rw [← exp_zero, exp_lt_exp]
 lemma exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0 :=
 by rw [← exp_zero, exp_lt_exp]
 
+/-- `real.cosh` is always positive -/
+lemma cosh_pos (x : ℝ) : 0 < real.cosh x :=
+(cosh_eq x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x)))
+
 end real
 
 namespace complex