From 38ab7a0f6a1ed378e0676e73b183c6a5e24a889b Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sat, 15 Aug 2020 19:36:05 +0100 Subject: [PATCH 01/59] Added sinh.lean --- src/analysis/special_functions/arsinh.lean | 190 +++++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 src/analysis/special_functions/arsinh.lean diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean new file mode 100644 index 0000000000000..838b68789b199 --- /dev/null +++ b/src/analysis/special_functions/arsinh.lean @@ -0,0 +1,190 @@ +/- +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 +import data.real.basic +import analysis.special_functions.pow + +open real +local attribute [pp_nodot] real.log +noncomputable theory + +/-! +# Inverse of the sinh function + +In this file we prove that sinh is bijective and hence has an +inverse, arsinh. + +## Main Results + +- `sinm_injective`: The proof that `sinm` is injective +- `sinm_surjective`: The proof that `sinm` is surjective +- `sinm_bijective`: The proof `sinm` is bijective + +## Notation + +- `arsinh`: The inverse function of `sinm` + +## Tags + +arsinh, sinh injective, sinh bijective, sinh surjective +-/ + +/-- The real definition of `cosh`-/ +lemma cosh_def (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := +by simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; + ring + +/-- The real definition of `sinh`-/ +lemma sinh_def (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := +by simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; + ring + +/-- `real.cosh` is positive-/ +lemma cosh_pos (x : ℝ) : 0 < real.cosh x := +(cosh_def x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) + +/-- `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) + +/-- `arsinh` is defined using a logarithm-/ +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 + (1 + x^2).sqrt) = - x + (1 + x^2).sqrt := +begin + have H : (x - (1 + x^2).sqrt)/((x - (1 + x^2).sqrt) * (x + (1 + x^2).sqrt)) = -x + (1 + x^2).sqrt, + { have G : (x - (1 + x^2).sqrt) * (x + (1 + x^2).sqrt) = -1, + { ring, + rw sqr_sqrt, + { ring }, + { linarith [pow_two_nonneg x]} }, + rw G, + ring }, + rw [division_def, mul_inv', ←mul_assoc, mul_comm (x - sqrt (1 + x ^ 2)), inv_mul_cancel] at H, + rw one_mul at H, + rw [division_def, one_mul], + exact H, + { intros fx, + rw sub_eq_zero at fx, + have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by { rw fx.symm }, + rw sqr_sqrt at fx_sq, + linarith, + have G : 0 ≤ x^2 := by {apply pow_two_nonneg}, + linarith } +end + +private lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt(b^2 + 1) := +begin + by_cases hb : 0 ≤ b, + conv { to_lhs, rw ← sqrt_sqr hb }, + rw sqrt_lt, + linarith, + apply pow_two_nonneg, + have F : 0 ≤ b^2 := by { apply pow_two_nonneg }, + linarith, + rw not_le at hb, + apply lt_of_lt_of_le hb, + apply sqrt_nonneg, +end + +/-- `sinh` is surjective, `∀ b, ∃ a, sinh a = b`. In this case, we use `a = arsinh b` -/ +lemma sinh_surjective : function.surjective sinh := +begin + intro b, + use (arsinh b), + rw sinh_def, + unfold arsinh, + rw ←log_inv, + rw [exp_log, exp_log], + { rw [← one_mul ((b + sqrt (1 + b ^ 2))⁻¹), ←division_def, aux_lemma], + ring }, + { rw [← one_mul ((b + sqrt (1 + b ^ 2))⁻¹), ←division_def, aux_lemma], + ring, + rw [neg_add_eq_sub, sub_pos], + have H : b^2 < sqrt (b ^ 2 + 1)^2, + { rw sqr_sqrt, + linarith, + have F : 0 ≤ b^2 := by {apply pow_two_nonneg}, + linarith }, + exact b_lt_sqrt_b_sq_add_one b, + }, + { have H := b_lt_sqrt_b_sq_add_one (-b), + rw [neg_square, add_comm (b^2)] at H, + linarith }, +end + +/-- `sinh` is bijective, both injective and surjective-/ +lemma sinh_bijective : function.bijective sinh := +⟨sinh_injective, sinh_surjective⟩ + +/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ +lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := +begin + rw [sinh, cosh], + have := complex.cosh_sq_sub_sinh_sq x, + apply_fun complex.re at this, + 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] at this, + norm_num at this, + rwa [pow_two, pow_two], +end + +/-- 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}, + ring at G, + rw add_comm at G, + rw [G.symm, sqrt_sqr], + exact le_of_lt (cosh_pos x), +end + +/-- `arsinh` is a left inverse of `sinh` -/ +lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x := +begin + unfold arsinh, + rw sinh_def, + apply exp_injective, + rw exp_log, + { rw [← sinh_def, sqrt_one_add_sinh_sq, cosh_def, sinh_def], + ring }, + { rw [← sinh_def, sqrt_one_add_sinh_sq, cosh_def, sinh_def], + ring, + exact exp_pos x }, +end + +/-- `arsinh` is the right inverse of `sinh`-/ +lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := +begin + rw sinh_def, + unfold arsinh, + rw ←log_inv, + rw [exp_log, exp_log], + { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], + ring }, + { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], + ring, + rw [neg_add_eq_sub, sub_pos], + have H : x^2 < sqrt (x ^ 2 + 1)^2, + { rw sqr_sqrt, + linarith, + have F : 0 ≤ x^2 := by {apply pow_two_nonneg}, + linarith }, + exact b_lt_sqrt_b_sq_add_one x, + }, + { have H := b_lt_sqrt_b_sq_add_one (-x), + rw [neg_square, add_comm (x^2)] at H, + linarith }, +end From ada137d9035ceb18240a34647fbee44e5fbb33b9 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sat, 15 Aug 2020 20:26:02 +0100 Subject: [PATCH 02/59] Rejigged some lemmas --- src/analysis/special_functions/arsinh.lean | 21 --------------------- src/data/complex/exponential.lean | 22 ++++++++++++++++++++++ 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 838b68789b199..4f899393f3f95 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -32,27 +32,6 @@ inverse, arsinh. arsinh, sinh injective, sinh bijective, sinh surjective -/ -/-- The real definition of `cosh`-/ -lemma cosh_def (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := -by simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; - ring - -/-- The real definition of `sinh`-/ -lemma sinh_def (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := -by simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; - ring - -/-- `real.cosh` is positive-/ -lemma cosh_pos (x : ℝ) : 0 < real.cosh x := -(cosh_def x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) - -/-- `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) /-- `arsinh` is defined using a logarithm-/ def arsinh (x : ℝ) := log (x + sqrt(1 + x^2)) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index a01ef0d63aa77..70f312706668e 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -503,11 +503,22 @@ mul_div_cancel' _ two_ne_zero' lemma two_cosh : 2 * cosh x = exp x + exp (-x) := mul_div_cancel' _ two_ne_zero' +/-- The real definition of `sinh`-/ +lemma sinh_def (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := +by simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; + ring + @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh] @[simp] lemma sinh_neg : sinh (-x) = -sinh x := by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul] +/-- `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) + private lemma sinh_add_aux {a b c d : ℂ} : (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d) := by ring @@ -521,11 +532,22 @@ begin exact sinh_add_aux end +/-- The real definition of `cosh`-/ +lemma cosh_def (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := +by simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; + ring + @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh] @[simp] lemma cosh_neg : cosh (-x) = cosh x := by simp [add_comm, cosh, exp_neg] +/-- `real.cosh` is positive-/ +lemma cosh_pos (x : ℝ) : 0 < real.cosh x := +(cosh_def x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) + private lemma cosh_add_aux {a b c d : ℂ} : (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d) := by ring From 3bc5e7c2267ef02f8351b4768e9b76ae658375dc Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sat, 15 Aug 2020 20:27:44 +0100 Subject: [PATCH 03/59] Removed `arsinh` from notation and added it to results --- src/analysis/special_functions/arsinh.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 4f899393f3f95..a65d63ee20302 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -22,9 +22,6 @@ inverse, arsinh. - `sinm_injective`: The proof that `sinm` is injective - `sinm_surjective`: The proof that `sinm` is surjective - `sinm_bijective`: The proof `sinm` is bijective - -## Notation - - `arsinh`: The inverse function of `sinm` ## Tags From dee5af0e34e9cf2a07afa82c71f3074014c9013f Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 12:17:50 +0100 Subject: [PATCH 04/59] Update src/data/complex/exponential.lean Renamed `sinh_def` to `sinh_eq` Co-authored-by: Johan Commelin --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 70f312706668e..cea649cfacdff 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -504,7 +504,7 @@ lemma two_cosh : 2 * cosh x = exp x + exp (-x) := mul_div_cancel' _ two_ne_zero' /-- The real definition of `sinh`-/ -lemma sinh_def (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := +lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := by simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; From 0c068466b94d1d6daee485939002efd15f7d2f27 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 12:20:08 +0100 Subject: [PATCH 05/59] Update src/analysis/special_functions/arsinh.lean added space after `sqrt` in `b_lt_sqrt_b_sq_add_one` Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index a65d63ee20302..03e7d1fc225be 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -59,7 +59,7 @@ begin linarith } end -private lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt(b^2 + 1) := +private lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt (b^2 + 1) := begin by_cases hb : 0 ≤ b, conv { to_lhs, rw ← sqrt_sqr hb }, From 1a06848572ba6e4e90e68dc2863a3dba33cda970 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 12:22:28 +0100 Subject: [PATCH 06/59] added @[pp_nodot] to log --- src/analysis/special_functions/exp_log.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean index 173245000765e..c245e6112a32f 100644 --- a/src/analysis/special_functions/exp_log.lean +++ b/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 := From a3129280d93a044dc5b919ba3ae38d7f4d123b40 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 12:24:45 +0100 Subject: [PATCH 07/59] Removed .sqrt in favour of the sqrt (f x) --- src/analysis/special_functions/arsinh.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 03e7d1fc225be..a4ca4fad934e0 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -36,10 +36,10 @@ 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 + (1 + x^2).sqrt) = - x + (1 + x^2).sqrt := +private lemma aux_lemma (x : ℝ) : 1/(sqrt (x + (1 + x^2)) = - x + sqrt (1 + x^2) := begin - have H : (x - (1 + x^2).sqrt)/((x - (1 + x^2).sqrt) * (x + (1 + x^2).sqrt)) = -x + (1 + x^2).sqrt, - { have G : (x - (1 + x^2).sqrt) * (x + (1 + x^2).sqrt) = -1, + have H : (x - sqrt (1 + x^2))/((x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2))) = -x + sqrt (1 + x^2), + { have G : (x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2)) = -1, { ring, rw sqr_sqrt, { ring }, From 24923cf9e9bcea09be128c4f0f1a19b44be4fbfa Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 12:26:37 +0100 Subject: [PATCH 08/59] added def to arsinh docstring --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index a4ca4fad934e0..4efda84320f41 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -30,7 +30,7 @@ arsinh, sinh injective, sinh bijective, sinh surjective -/ -/-- `arsinh` is defined using a logarithm-/ +/-- `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` -/ From c1a06f31704f8c60abcbac256c48d1dde02c9446 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:02:07 +0100 Subject: [PATCH 09/59] Update src/analysis/special_functions/arsinh.lean removed braces around apply `pow_two_nonneg` Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 4efda84320f41..e491ff22b1043 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -90,7 +90,7 @@ begin have H : b^2 < sqrt (b ^ 2 + 1)^2, { rw sqr_sqrt, linarith, - have F : 0 ≤ b^2 := by {apply pow_two_nonneg}, + have F : 0 ≤ b^2 := by apply pow_two_nonneg, linarith }, exact b_lt_sqrt_b_sq_add_one b, }, From f4bbe0d7f12b487a8360f2e961e81ba14c44b186 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:04:51 +0100 Subject: [PATCH 10/59] Update src/analysis/special_functions/arsinh.lean Moved braces on line 95 Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index e491ff22b1043..53cdedacb832d 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -92,8 +92,7 @@ begin linarith, have F : 0 ≤ b^2 := by apply pow_two_nonneg, linarith }, - exact b_lt_sqrt_b_sq_add_one b, - }, + exact b_lt_sqrt_b_sq_add_one b }, { have H := b_lt_sqrt_b_sq_add_one (-b), rw [neg_square, add_comm (b^2)] at H, linarith }, From 238a190a716f909dcae5c25d0be47d28e1813ad3 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:12:45 +0100 Subject: [PATCH 11/59] Update src/analysis/special_functions/arsinh.lean Replaced `sinm` with `sihn` Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 53cdedacb832d..2366d5c86c429 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -19,7 +19,7 @@ inverse, arsinh. ## Main Results -- `sinm_injective`: The proof that `sinm` is injective +- `sinh_injective`: The proof that `sinh` is injective - `sinm_surjective`: The proof that `sinm` is surjective - `sinm_bijective`: The proof `sinm` is bijective - `arsinh`: The inverse function of `sinm` From 8ecda924b51d41c9ae6f1d222cabf01684707163 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:17:40 +0100 Subject: [PATCH 12/59] Updated sinh/cosh_def to sinh/cosh_eq --- src/analysis/special_functions/arsinh.lean | 10 +++++----- src/data/complex/exponential.lean | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 2366d5c86c429..9ac56428ff981 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -78,7 +78,7 @@ lemma sinh_surjective : function.surjective sinh := begin intro b, use (arsinh b), - rw sinh_def, + rw sinh_eq, unfold arsinh, rw ←log_inv, rw [exp_log, exp_log], @@ -130,12 +130,12 @@ end lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x := begin unfold arsinh, - rw sinh_def, + rw sinh_eq, apply exp_injective, rw exp_log, - { rw [← sinh_def, sqrt_one_add_sinh_sq, cosh_def, sinh_def], + { rw [← sinh_eq, sqrt_one_add_sinh_sq, cosh_eq, sinh_eq], ring }, - { rw [← sinh_def, sqrt_one_add_sinh_sq, cosh_def, sinh_def], + { rw [← sinh_eq, sqrt_one_add_sinh_sq, cosh_eq, sinh_eq], ring, exact exp_pos x }, end @@ -143,7 +143,7 @@ end /-- `arsinh` is the right inverse of `sinh`-/ lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := begin - rw sinh_def, + rw sinh_eq, unfold arsinh, rw ←log_inv, rw [exp_log, exp_log], diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index cea649cfacdff..ae743bf141284 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -533,7 +533,7 @@ begin end /-- The real definition of `cosh`-/ -lemma cosh_def (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := +lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := by simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; @@ -546,7 +546,7 @@ by simp [add_comm, cosh, exp_neg] /-- `real.cosh` is positive-/ lemma cosh_pos (x : ℝ) : 0 < real.cosh x := -(cosh_def x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) +(cosh_eq x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) private lemma cosh_add_aux {a b c d : ℂ} : (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d) := by ring From 3d7a6a54098cf327678a3068801e2e5bad749824 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:27:42 +0100 Subject: [PATCH 13/59] Added braces and commas to sinh/cosh_eq --- src/data/complex/exponential.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index ae743bf141284..73a5040b11ef8 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -505,10 +505,10 @@ mul_div_cancel' _ two_ne_zero' /-- The real definition of `sinh`-/ lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := -by simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, +by {simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; - ring + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], + ring} @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh] @@ -534,10 +534,10 @@ end /-- The real definition of `cosh`-/ lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := -by simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, +by {simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq]; - ring + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], + ring} @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh] From 53e82319a2e40ff8aee5230f90987f8cb7bf6723 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:30:18 +0100 Subject: [PATCH 14/59] removed braces after single command `have`s --- src/analysis/special_functions/arsinh.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 9ac56428ff981..414d0984a6a41 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -52,10 +52,10 @@ begin exact H, { intros fx, rw sub_eq_zero at fx, - have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by { rw fx.symm }, + have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by rw fx.symm, rw sqr_sqrt at fx_sq, linarith, - have G : 0 ≤ x^2 := by {apply pow_two_nonneg}, + have G : 0 ≤ x^2 := by apply pow_two_nonneg, linarith } end @@ -66,7 +66,7 @@ begin rw sqrt_lt, linarith, apply pow_two_nonneg, - have F : 0 ≤ b^2 := by { apply pow_two_nonneg }, + have F : 0 ≤ b^2 := by apply pow_two_nonneg, linarith, rw not_le at hb, apply lt_of_lt_of_le hb, @@ -119,7 +119,7 @@ end 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}, + have G : cosh x ^ 2 - sinh x ^ 2 + sinh x ^ 2 = 1 + sinh x ^ 2 := by rw H, ring at G, rw add_comm at G, rw [G.symm, sqrt_sqr], @@ -155,7 +155,7 @@ begin have H : x^2 < sqrt (x ^ 2 + 1)^2, { rw sqr_sqrt, linarith, - have F : 0 ≤ x^2 := by {apply pow_two_nonneg}, + have F : 0 ≤ x^2 := by apply pow_two_nonneg, linarith }, exact b_lt_sqrt_b_sq_add_one x, }, From 207149424c4c71994719bb17e94970450bd899ca Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:35:18 +0100 Subject: [PATCH 15/59] added extra tags --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 414d0984a6a41..fe811ee99db97 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -26,7 +26,7 @@ inverse, arsinh. ## Tags -arsinh, sinh injective, sinh bijective, sinh surjective +arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective -/ From 79bb7b67121e80e6a498e17ec48fccf27fcf4b07 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:37:13 +0100 Subject: [PATCH 16/59] Update src/analysis/special_functions/arsinh.lean Co-authored-by: Floris van Doorn --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 414d0984a6a41..fe811ee99db97 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -26,7 +26,7 @@ inverse, arsinh. ## Tags -arsinh, sinh injective, sinh bijective, sinh surjective +arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective -/ From a69e47e041031ea85eabd7afd3672551656bc3ac Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:38:13 +0100 Subject: [PATCH 17/59] replaced sinm with sinh --- src/analysis/special_functions/arsinh.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index fe811ee99db97..24e4e1192b033 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -20,9 +20,9 @@ inverse, arsinh. ## Main Results - `sinh_injective`: The proof that `sinh` is injective -- `sinm_surjective`: The proof that `sinm` is surjective -- `sinm_bijective`: The proof `sinm` is bijective -- `arsinh`: The inverse function of `sinm` +- `sinm_surjective`: The proof that `sinh` is surjective +- `sinm_bijective`: The proof `sinh` is bijective +- `arsinh`: The inverse function of `sinh` ## Tags From c6a8bc883336e3a23aa6daeed8431c462eeae975 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:40:10 +0100 Subject: [PATCH 18/59] updared aux_lemma to remove error --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 24e4e1192b033..92fa884e36102 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -36,7 +36,7 @@ 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/(sqrt (x + (1 + x^2)) = - x + sqrt (1 + x^2) := +private lemma aux_lemma (x : ℝ) : 1 / (x + sqrt(1 + x^2)) = - x + sqrt(1 + x^2) := begin have H : (x - sqrt (1 + x^2))/((x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2))) = -x + sqrt (1 + x^2), { have G : (x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2)) = -1, From 0a3d0841068a5765635b9b26962085bd28bf1192 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:41:28 +0100 Subject: [PATCH 19/59] moved real.cosh_sq_add_sinh_sq --- src/analysis/special_functions/arsinh.lean | 13 ------------- src/data/complex/exponential.lean | 16 +++++++++++++++- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 92fa884e36102..ccfa8a6b43146 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -102,19 +102,6 @@ end lemma sinh_bijective : function.bijective sinh := ⟨sinh_injective, sinh_surjective⟩ -/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ -lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := -begin - rw [sinh, cosh], - have := complex.cosh_sq_sub_sinh_sq x, - apply_fun complex.re at this, - 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] at this, - norm_num at this, - rwa [pow_two, pow_two], -end - /-- 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 diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 73a5040b11ef8..e3461a83c3942 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -629,7 +629,7 @@ lemma cosh_sub_sinh : cosh x - sinh x = exp (-x) := by rw [← mul_right_inj' (@two_ne_zero' ℂ _ _ _), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul] -lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := +lemma _sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero] @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin] @@ -739,6 +739,20 @@ eq.trans (by rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]) (cosh_sq_sub_sinh_sq (x * I)) +/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ +lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := +begin + rw [sinh, cosh], + have := complex.cosh_sq_sub_sinh_sq x, + apply_fun complex.re at this, + 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] at this, + norm_num at this, + rwa [pow_two, pow_two], +end + + lemma cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 := by rw [two_mul, cos_add, ← pow_two, ← pow_two] From e643c7d6710e39a9996d4d7451e2dc87ba3465ab Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:46:26 +0100 Subject: [PATCH 20/59] reduced imports --- src/analysis/special_functions/arsinh.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index ccfa8a6b43146..fd2d9302202c7 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -4,8 +4,6 @@ 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 -import data.real.basic -import analysis.special_functions.pow open real local attribute [pp_nodot] real.log From 457af704da9a057083014af8c63f00a95f64cae0 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 13:49:24 +0100 Subject: [PATCH 21/59] added braces to aux_lemma --- src/analysis/special_functions/arsinh.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index fd2d9302202c7..46eb846cbb83f 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -50,11 +50,11 @@ begin exact H, { intros fx, rw sub_eq_zero at fx, - have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by rw fx.symm, + have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by { rw fx.symm }, rw sqr_sqrt at fx_sq, - linarith, - have G : 0 ≤ x^2 := by apply pow_two_nonneg, - linarith } + { linarith }, + { have G : 0 ≤ x^2 := by {apply pow_two_nonneg}, + linarith }} end private lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt (b^2 + 1) := From 9752231b7b96905c6a1f9263aacb6b11b1b79c18 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 14:10:30 +0100 Subject: [PATCH 22/59] added braces to b_lt_b_sq_add_one --- src/analysis/special_functions/arsinh.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 46eb846cbb83f..fccbcf61d4ddf 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -64,8 +64,8 @@ begin rw sqrt_lt, linarith, apply pow_two_nonneg, - have F : 0 ≤ b^2 := by apply pow_two_nonneg, - linarith, + have F : 0 ≤ b^2 := by { apply pow_two_nonneg }, + { linarith }, rw not_le at hb, apply lt_of_lt_of_le hb, apply sqrt_nonneg, From 46486eb2a02897f31047e29568a5fe6f395735a2 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 14:11:45 +0100 Subject: [PATCH 23/59] updated sinh_surjective --- src/analysis/special_functions/arsinh.lean | 28 +++------------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index fccbcf61d4ddf..8d80040ebb5a4 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -50,7 +50,7 @@ begin exact H, { intros fx, rw sub_eq_zero at fx, - have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by { rw fx.symm }, + have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by rw fx.symm, rw sqr_sqrt at fx_sq, { linarith }, { have G : 0 ≤ x^2 := by {apply pow_two_nonneg}, @@ -64,7 +64,7 @@ begin rw sqrt_lt, linarith, apply pow_two_nonneg, - have F : 0 ≤ b^2 := by { apply pow_two_nonneg }, + have F : 0 ≤ b^2 := by apply pow_two_nonneg, { linarith }, rw not_le at hb, apply lt_of_lt_of_le hb, @@ -72,29 +72,7 @@ begin end /-- `sinh` is surjective, `∀ b, ∃ a, sinh a = b`. In this case, we use `a = arsinh b` -/ -lemma sinh_surjective : function.surjective sinh := -begin - intro b, - use (arsinh b), - rw sinh_eq, - unfold arsinh, - rw ←log_inv, - rw [exp_log, exp_log], - { rw [← one_mul ((b + sqrt (1 + b ^ 2))⁻¹), ←division_def, aux_lemma], - ring }, - { rw [← one_mul ((b + sqrt (1 + b ^ 2))⁻¹), ←division_def, aux_lemma], - ring, - rw [neg_add_eq_sub, sub_pos], - have H : b^2 < sqrt (b ^ 2 + 1)^2, - { rw sqr_sqrt, - linarith, - have F : 0 ≤ b^2 := by apply pow_two_nonneg, - linarith }, - exact b_lt_sqrt_b_sq_add_one b }, - { have H := b_lt_sqrt_b_sq_add_one (-b), - rw [neg_square, add_comm (b^2)] at H, - linarith }, -end +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 := From 2eee37a5f130ee7c89f166a8eef7d0f3ba43519e Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 14:18:42 +0100 Subject: [PATCH 24/59] relocated real.cosh_sq_sub_sinh_sq --- src/data/complex/exponential.lean | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index e3461a83c3942..fcc526720b7a8 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -632,6 +632,19 @@ by rw [← mul_right_inj' (@two_ne_zero' ℂ _ _ _), mul_sub, lemma _sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero] +/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ +lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := +begin + rw [sinh, cosh], + have := complex.cosh_sq_sub_sinh_sq x, + apply_fun complex.re at this, + 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] at this, + norm_num at this, + rwa [pow_two, pow_two], +end + @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin] @[simp] lemma sin_neg : sin (-x) = -sin x := @@ -739,20 +752,6 @@ eq.trans (by rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]) (cosh_sq_sub_sinh_sq (x * I)) -/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ -lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := -begin - rw [sinh, cosh], - have := complex.cosh_sq_sub_sinh_sq x, - apply_fun complex.re at this, - 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] at this, - norm_num at this, - rwa [pow_two, pow_two], -end - - lemma cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 := by rw [two_mul, cos_add, ← pow_two, ← pow_two] From 2ed1a1ac92532f1407cdac81870590647ed9137f Mon Sep 17 00:00:00 2001 From: James Arthur Date: Sun, 16 Aug 2020 14:21:40 +0100 Subject: [PATCH 25/59] relocated arsinh --- src/analysis/special_functions/arsinh.lean | 48 +++++++++++----------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 8d80040ebb5a4..f7ec341ee17ed 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -71,6 +71,30 @@ begin apply sqrt_nonneg, end +/-- `arsinh` is the right inverse of `sinh`-/ +lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := +begin + rw sinh_eq, + unfold arsinh, + rw ←log_inv, + rw [exp_log, exp_log], + { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], + ring }, + { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], + ring, + rw [neg_add_eq_sub, sub_pos], + have H : x^2 < sqrt (x ^ 2 + 1)^2, + { rw sqr_sqrt, + linarith, + have F : 0 ≤ x^2 := by apply pow_two_nonneg, + linarith }, + exact b_lt_sqrt_b_sq_add_one x, + }, + { have H := b_lt_sqrt_b_sq_add_one (-x), + rw [neg_square, add_comm (x^2)] at H, + linarith }, +end + /-- `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 @@ -102,27 +126,3 @@ begin ring, exact exp_pos x }, end - -/-- `arsinh` is the right inverse of `sinh`-/ -lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := -begin - rw sinh_eq, - unfold arsinh, - rw ←log_inv, - rw [exp_log, exp_log], - { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], - ring }, - { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], - ring, - rw [neg_add_eq_sub, sub_pos], - have H : x^2 < sqrt (x ^ 2 + 1)^2, - { rw sqr_sqrt, - linarith, - have F : 0 ≤ x^2 := by apply pow_two_nonneg, - linarith }, - exact b_lt_sqrt_b_sq_add_one x, - }, - { have H := b_lt_sqrt_b_sq_add_one (-x), - rw [neg_square, add_comm (x^2)] at H, - linarith }, -end From e8566a2cf1889cc3c7ab23a2c3bd2fb8a9b1cd84 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 10:15:49 +0100 Subject: [PATCH 26/59] Update src/analysis/special_functions/arsinh.lean Removed local attribute Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index f7ec341ee17ed..d2f3df506069d 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -6,7 +6,6 @@ Authors: James Arthur, Chris Hughes, Shing Tak Lam. import analysis.special_functions.trigonometric open real -local attribute [pp_nodot] real.log noncomputable theory /-! From cf37673563caa87106c2b41c479bb129454791ec Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 10:16:20 +0100 Subject: [PATCH 27/59] Update src/data/complex/exponential.lean Renamed Co-authored-by: Shing Tak Lam --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index fcc526720b7a8..e928e220f15ab 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -629,7 +629,7 @@ lemma cosh_sub_sinh : cosh x - sinh x = exp (-x) := by rw [← mul_right_inj' (@two_ne_zero' ℂ _ _ _), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul] -lemma _sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := +lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero] /-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ From 04bbe11e2424ce1885be91491ebe6777a8a2d406 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 10:16:51 +0100 Subject: [PATCH 28/59] Update src/analysis/special_functions/arsinh.lean Removed `ring` Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index d2f3df506069d..18315798cafad 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -106,8 +106,7 @@ 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, - ring at G, - rw add_comm at G, + rw sub_add_cancel at G, rw [G.symm, sqrt_sqr], exact le_of_lt (cosh_pos x), end From 92666be1b29d49ec55783ec005033cb7246992d5 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 10:17:27 +0100 Subject: [PATCH 29/59] Update src/analysis/special_functions/arsinh.lean Replaced G.symm with \l G Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 18315798cafad..e9f75349f29f0 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -107,7 +107,7 @@ 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.symm, sqrt_sqr], + rw [←G, sqrt_sqr], exact le_of_lt (cosh_pos x), end From 72c83b9a7c8d554b67b703502312e244a6f3863f Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 10:18:03 +0100 Subject: [PATCH 30/59] Update src/analysis/special_functions/arsinh.lean Updated the names in Key Results Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index e9f75349f29f0..434bea0113769 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -17,8 +17,8 @@ inverse, arsinh. ## Main Results - `sinh_injective`: The proof that `sinh` is injective -- `sinm_surjective`: The proof that `sinh` is surjective -- `sinm_bijective`: The proof `sinh` is bijective +- `sinh_surjective`: The proof that `sinh` is surjective +- `sinh_bijective`: The proof `sinh` is bijective - `arsinh`: The inverse function of `sinh` ## Tags From 25a685f4520c425cd106460f8655c25ee7a8c2d9 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 11:18:16 +0100 Subject: [PATCH 31/59] moved defs --- src/data/complex/exponential.lean | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index fcc526720b7a8..f2df3c77389d8 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -503,13 +503,6 @@ mul_div_cancel' _ two_ne_zero' lemma two_cosh : 2 * cosh x = exp x + exp (-x) := mul_div_cancel' _ two_ne_zero' -/-- The real definition of `sinh`-/ -lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := -by {simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], - ring} - @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh] @[simp] lemma sinh_neg : sinh (-x) = -sinh x := @@ -532,13 +525,6 @@ begin exact sinh_add_aux end -/-- The real definition of `cosh`-/ -lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := -by {simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], - ring} - @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh] @[simp] lemma cosh_neg : cosh (-x) = cosh x := @@ -897,6 +883,13 @@ 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 real definition of `sinh`-/ +lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := +by {simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], + ring} + @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh] @[simp] lemma sinh_neg : sinh (-x) = -sinh x := @@ -905,6 +898,13 @@ 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 real definition of `cosh`-/ +lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := +by {simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, + bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, + complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], + ring} + @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh] @[simp] lemma cosh_neg : cosh (-x) = cosh x := From 78e560020f81b1b615f0a432a7875d2a6fbe0e97 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 11:25:54 +0100 Subject: [PATCH 32/59] Trying to make lean happy --- .../special_functions/trigonometric.lean | 4 +++ src/data/complex/exponential.lean | 36 ++++++++----------- 2 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean index a428fd3dcfe96..3735418ac5ec4 100644 --- a/src/analysis/special_functions/trigonometric.lean +++ b/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 diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 0e97e5d34a3d9..15dbf47a7bbce 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -508,10 +508,6 @@ mul_div_cancel' _ two_ne_zero' @[simp] lemma sinh_neg : sinh (-x) = -sinh x := by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul] -/-- `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) - private lemma sinh_add_aux {a b c d : ℂ} : (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d) := by ring @@ -530,10 +526,6 @@ end @[simp] lemma cosh_neg : cosh (-x) = cosh x := by simp [add_comm, cosh, exp_neg] -/-- `real.cosh` is positive-/ -lemma cosh_pos (x : ℝ) : 0 < real.cosh x := -(cosh_eq x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x))) - private lemma cosh_add_aux {a b c d : ℂ} : (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d) := by ring @@ -618,19 +610,6 @@ by rw [← mul_right_inj' (@two_ne_zero' ℂ _ _ _), mul_sub, lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 := by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero] -/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ -lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := -begin - rw [sinh, cosh], - have := complex.cosh_sq_sub_sinh_sq x, - apply_fun complex.re at this, - 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] at this, - norm_num at this, - rwa [pow_two, pow_two], -end - @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin] @[simp] lemma sin_neg : sin (-x) = -sin x := @@ -919,6 +898,17 @@ 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] +/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ +lemma real.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] @@ -979,6 +969,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 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 From d0df08ba964695d69c9d3f1fd284a03a3a75be92 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 11:57:00 +0100 Subject: [PATCH 33/59] removed real on cosh_sq_sih_sq --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 15dbf47a7bbce..ae46713ddc825 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -899,7 +899,7 @@ 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] /-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ -lemma real.cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := +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), From fefc5bb404c7720e7f15825bf49640be4634c0ae Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:01:03 +0100 Subject: [PATCH 34/59] Update src/analysis/special_functions/arsinh.lean Co-authored-by: Shing Tak Lam --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 434bea0113769..16bbfaee332c5 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -111,7 +111,7 @@ begin exact le_of_lt (cosh_pos x), end -/-- `arsinh` is a left inverse of `sinh` -/ +/-- `arsinh` is the left inverse of `sinh` -/ lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x := begin unfold arsinh, From 23e01e1221e97f4cdcd097bb14b7ef4a2cf72806 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:01:36 +0100 Subject: [PATCH 35/59] Update src/data/complex/exponential.lean Co-authored-by: Shing Tak Lam --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index ae46713ddc825..059577ad78be3 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -862,7 +862,7 @@ 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 real definition of `sinh`-/ +/-- The definition of `sinh` in terms of `exp` -/ lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 := by {simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, From 13d337a969ed8c01d1aba0cd3a403b4877b9ae28 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:01:52 +0100 Subject: [PATCH 36/59] Update src/data/complex/exponential.lean Co-authored-by: Shing Tak Lam --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 059577ad78be3..4c75970945072 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -877,7 +877,7 @@ 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 real definition of `cosh`-/ +/-- The definition of `cosh` in terms of `exp`. -/ lemma cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 := by {simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, From beb7269b5c648d1362e1289244e82477319c5326 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:02:16 +0100 Subject: [PATCH 37/59] Update src/data/complex/exponential.lean Co-authored-by: Shing Tak Lam --- src/data/complex/exponential.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 4c75970945072..7322462c137ec 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -969,7 +969,7 @@ 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 positive-/ +/-- `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))) From 72871088c9e53b830bf45d888e615c94ccb42b11 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:24:53 +0100 Subject: [PATCH 38/59] removed docstring on cosh_sq_sub_sinh_sq --- src/data/complex/exponential.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index ae46713ddc825..54b4e66c71a39 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -898,7 +898,6 @@ 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] -/-- A real version of `complex.cosh_sq_sub_sinh_sq`-/ lemma cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 := begin rw [sinh, cosh], From 827ae2c2b773dee1f88834d8818e81eb8b1d8816 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:26:53 +0100 Subject: [PATCH 39/59] Moved code into one rw on line 78 --- src/analysis/special_functions/arsinh.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 16bbfaee332c5..c3d72bb3e5c70 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -75,8 +75,7 @@ lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := begin rw sinh_eq, unfold arsinh, - rw ←log_inv, - rw [exp_log, exp_log], + rw [←log_inv, exp_log, exp_log], { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], ring }, { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], From 8167571b6e418da61215cdd5d4b656637166e12e Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 13:58:06 +0100 Subject: [PATCH 40/59] Update src/analysis/special_functions/arsinh.lean Co-authored-by: Kenny Lau --- src/analysis/special_functions/arsinh.lean | 25 +++++----------------- 1 file changed, 5 insertions(+), 20 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index c3d72bb3e5c70..2195eb09d81be 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -33,27 +33,12 @@ 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) := +private lemma aux_lemma (x : ℝ) : 1 / (x + sqrt (1 + x^2)) = -x + sqrt (1 + x^2) := begin - have H : (x - sqrt (1 + x^2))/((x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2))) = -x + sqrt (1 + x^2), - { have G : (x - sqrt (1 + x^2)) * (x + sqrt (1 + x^2)) = -1, - { ring, - rw sqr_sqrt, - { ring }, - { linarith [pow_two_nonneg x]} }, - rw G, - ring }, - rw [division_def, mul_inv', ←mul_assoc, mul_comm (x - sqrt (1 + x ^ 2)), inv_mul_cancel] at H, - rw one_mul at H, - rw [division_def, one_mul], - exact H, - { intros fx, - rw sub_eq_zero at fx, - have fx_sq : x^2 = (sqrt (1 + x ^ 2)) ^ 2 := by rw fx.symm, - rw sqr_sqrt at fx_sq, - { linarith }, - { have G : 0 ≤ x^2 := by {apply pow_two_nonneg}, - linarith }} + 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_sq_add_one (b : ℝ) : b < sqrt (b^2 + 1) := From d5661986b2a833de550e2070946b826743cb8509 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:22:38 +0100 Subject: [PATCH 41/59] Update src/analysis/special_functions/arsinh.lean add full stop and space Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 2195eb09d81be..7b156f09ef227 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -55,7 +55,7 @@ begin apply sqrt_nonneg, end -/-- `arsinh` is the right inverse of `sinh`-/ +/-- `arsinh` is the right inverse of `sinh`. -/ lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := begin rw sinh_eq, From 5bb4ec4be06db98dbdabdf230885fb940357ef28 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:23:06 +0100 Subject: [PATCH 42/59] Update src/analysis/special_functions/arsinh.lean Added full stop Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 7b156f09ef227..e696c706632d7 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -1,7 +1,7 @@ /- 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. +Authors: James Arthur, Chris Hughes, Shing Tak Lam -/ import analysis.special_functions.trigonometric From a7b0f1348ac0274fdd134e8b7d2f914e18035f29 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:23:40 +0100 Subject: [PATCH 43/59] Update src/analysis/special_functions/arsinh.lean added full stop Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index e696c706632d7..b3e8a3d7710b1 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -81,7 +81,7 @@ end /-- `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-/ +/-- `sinh` is bijective, both injective and surjective. -/ lemma sinh_bijective : function.bijective sinh := ⟨sinh_injective, sinh_surjective⟩ From 5fb85ac331885b2aac7a1e6ba21e8418d57b73e4 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:29:37 +0100 Subject: [PATCH 44/59] Update src/analysis/special_functions/trigonometric.lean added spaces and removed semi colon Co-authored-by: Markus Himmel --- src/analysis/special_functions/trigonometric.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean index 3735418ac5ec4..9bf9762cac29b 100644 --- a/src/analysis/special_functions/trigonometric.lean +++ b/src/analysis/special_functions/trigonometric.lean @@ -350,7 +350,7 @@ 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) +strict_mono_of_deriv_pos differentiable_sinh (by { rw [real.deriv_sinh], exact cosh_pos }) end real From ffa53ea489e6513b2354e6be71e861db0d2eab3e Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:30:00 +0100 Subject: [PATCH 45/59] Update src/analysis/special_functions/trigonometric.lean added full stop and space Co-authored-by: Markus Himmel --- src/analysis/special_functions/trigonometric.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean index 9bf9762cac29b..82a1c9fbb9e78 100644 --- a/src/analysis/special_functions/trigonometric.lean +++ b/src/analysis/special_functions/trigonometric.lean @@ -348,7 +348,7 @@ funext $ λ x, (has_deriv_at_cosh x).deriv lemma continuous_cosh : continuous cosh := differentiable_cosh.continuous -/-- `sinh` is strictly monotone-/ +/-- `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 }) From a2078af8ce8d753db849e6b59fb5672951a536cd Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:30:15 +0100 Subject: [PATCH 46/59] Update src/data/complex/exponential.lean added spaces Co-authored-by: Markus Himmel --- src/data/complex/exponential.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 1e9db64660731..d34c6954e7f80 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -879,10 +879,10 @@ 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 := -by {simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, +by { simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], - ring} + ring } @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh] From 3a99cd60c904f720800ef612d724a5ea670c7999 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:30:31 +0100 Subject: [PATCH 47/59] Update src/analysis/special_functions/arsinh.lean added space after sqrt Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index b3e8a3d7710b1..d2ea6145ad0ff 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -28,7 +28,7 @@ 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)) +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 From c01097200c23eba111a74ed9a24ca3a40cf55ed4 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:30:50 +0100 Subject: [PATCH 48/59] Update src/analysis/special_functions/arsinh.lean removed new line brace Co-authored-by: Markus Himmel --- src/analysis/special_functions/arsinh.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index d2ea6145ad0ff..fcb6163c3f062 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -71,8 +71,7 @@ begin linarith, have F : 0 ≤ x^2 := by apply pow_two_nonneg, linarith }, - exact b_lt_sqrt_b_sq_add_one x, - }, + exact b_lt_sqrt_b_sq_add_one x }, { have H := b_lt_sqrt_b_sq_add_one (-x), rw [neg_square, add_comm (x^2)] at H, linarith }, From 1f9edf58d7983291a737fe65bdc71e2e25b6a054 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:39:51 +0100 Subject: [PATCH 49/59] Update src/analysis/special_functions/arsinh.lean added spaces around `^` Co-authored-by: Kenny Lau --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index fcb6163c3f062..e16efcf4a4ae5 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -33,7 +33,7 @@ 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) := +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), From d15b0886fe0ab59cbe0124f3ee45dd32563b88cc Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:40:22 +0100 Subject: [PATCH 50/59] Update src/analysis/special_functions/arsinh.lean rewritten proof Co-authored-by: Kenny Lau --- src/analysis/special_functions/arsinh.lean | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index e16efcf4a4ae5..f6cdf616151ab 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -41,19 +41,11 @@ begin mul_self_sqrt this, pow_two, add_sub_cancel] end -private lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt (b^2 + 1) := -begin - by_cases hb : 0 ≤ b, - conv { to_lhs, rw ← sqrt_sqr hb }, - rw sqrt_lt, - linarith, - apply pow_two_nonneg, - have F : 0 ≤ b^2 := by apply pow_two_nonneg, - { linarith }, - rw not_le at hb, - apply lt_of_lt_of_le hb, - apply sqrt_nonneg, -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 _) /-- `arsinh` is the right inverse of `sinh`. -/ lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := From 3cf9ff0ec6380344091bcaf44db674be059104f0 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:40:48 +0100 Subject: [PATCH 51/59] Update src/data/complex/exponential.lean rewritten proof Co-authored-by: Kenny Lau --- src/data/complex/exponential.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index d34c6954e7f80..c9f26fe84fd1e 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -864,10 +864,8 @@ 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 := -by {simp only [sinh, complex.sinh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.sub_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], - ring} +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] From 8851ea6cfbc36e70c67df410c003a523ead7b1f0 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:41:32 +0100 Subject: [PATCH 52/59] Update src/analysis/special_functions/arsinh.lean simplifies proof Co-authored-by: Kenny Lau --- src/analysis/special_functions/arsinh.lean | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index f6cdf616151ab..b003c1c3b81ff 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -88,14 +88,4 @@ end /-- `arsinh` is the left inverse of `sinh` -/ lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x := -begin - unfold arsinh, - rw sinh_eq, - apply exp_injective, - rw exp_log, - { rw [← sinh_eq, sqrt_one_add_sinh_sq, cosh_eq, sinh_eq], - ring }, - { rw [← sinh_eq, sqrt_one_add_sinh_sq, cosh_eq, sinh_eq], - ring, - exact exp_pos x }, -end +function.right_inverse_of_injective_of_left_inverse sinh_injective arsinh_sinh x From 5dfa6d5f2101b96875c4b33d2011d4317a260d60 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Mon, 17 Aug 2020 14:46:55 +0100 Subject: [PATCH 53/59] added Kenny's code --- src/analysis/special_functions/arsinh.lean | 29 +++++++--------------- 1 file changed, 9 insertions(+), 20 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index b003c1c3b81ff..29bce0a815d88 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -47,27 +47,16 @@ calc b ... < sqrt (1 + b ^ 2) : (sqrt_lt (pow_two_nonneg _) (add_nonneg zero_le_one (pow_two_nonneg _))).2 (lt_one_add _) -/-- `arsinh` is the right inverse of `sinh`. -/ +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 := -begin - rw sinh_eq, - unfold arsinh, - rw [←log_inv, exp_log, exp_log], - { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], - ring }, - { rw [← one_mul ((x + sqrt (1 + x ^ 2))⁻¹), ←division_def, aux_lemma], - ring, - rw [neg_add_eq_sub, sub_pos], - have H : x^2 < sqrt (x ^ 2 + 1)^2, - { rw sqr_sqrt, - linarith, - have F : 0 ≤ x^2 := by apply pow_two_nonneg, - linarith }, - exact b_lt_sqrt_b_sq_add_one x }, - { have H := b_lt_sqrt_b_sq_add_one (-x), - rw [neg_square, add_comm (x^2)] at H, - linarith }, -end +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 From b75ab5f36e0d8680f851a4dfab9a14504be5ac57 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Tue, 18 Aug 2020 11:20:25 +0100 Subject: [PATCH 54/59] updated cosh_eq with a Kenny esc proof --- src/data/complex/exponential.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index c9f26fe84fd1e..c30cc77addcd3 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -877,10 +877,8 @@ 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 := -by { simp only [cosh, complex.cosh, complex.div_re, complex.exp_of_real_re, complex.one_re, - bit0_zero, add_zero, complex.add_re, euclidean_domain.zero_div, complex.bit0_re, - complex.one_im, complex.bit0_im, mul_zero, ← complex.of_real_neg, complex.norm_sq], - ring } +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] From d9f645c7dca20da9d72708d579e4c0747bef35f0 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Tue, 18 Aug 2020 12:48:32 +0100 Subject: [PATCH 55/59] added full stops and spaces to docstrings --- src/analysis/special_functions/arsinh.lean | 12 ++++++------ src/data/complex/exponential.lean | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 29bce0a815d88..7a78aceb57908 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -27,10 +27,10 @@ arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective -/ -/-- `arsinh` is defined using a logarithm, `arsinh x = log (x + sqrt(1 + x^2))` -/ +/-- `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` -/ +/-- `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) := @@ -51,21 +51,21 @@ 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`-/ +/-- `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` -/ +/-- `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` -/ +/-- 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, @@ -75,6 +75,6 @@ begin exact le_of_lt (cosh_pos x), end -/-- `arsinh` is the left inverse of `sinh` -/ +/-- `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 diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index c30cc77addcd3..a5b711ec11182 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -862,7 +862,7 @@ 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` -/ +/-- 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] From 745acc1e41e7efcac7b21b09ae1d0c0fee75bf38 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Tue, 18 Aug 2020 13:34:29 +0100 Subject: [PATCH 56/59] swapped the names of arinh_sinh and sinh_arsinh --- src/analysis/special_functions/arsinh.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 7a78aceb57908..4b7e13d94cc38 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -52,7 +52,7 @@ by { rw [← neg_neg b, ← sub_eq_neg_add, sub_pos, pow_two, neg_mul_neg, ← p exact b_lt_sqrt_b_one_add_sq (-b) } /-- `arsinh` is the right inverse of `sinh`. -/ -lemma arsinh_sinh (x : ℝ) : sinh (arsinh x) = x := +lemma sinh_arsinh (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, @@ -76,5 +76,5 @@ begin end /-- `arsinh` is the left inverse of `sinh`. -/ -lemma sinh_arsinh (x : ℝ) : arsinh (sinh x) = x := +lemma arsinh_sinh (x : ℝ) : arsinh (sinh x) = x := function.right_inverse_of_injective_of_left_inverse sinh_injective arsinh_sinh x From c8ec1084f89bddc481d3c04f371371c8273fbe81 Mon Sep 17 00:00:00 2001 From: James Arthur Date: Tue, 18 Aug 2020 13:41:54 +0100 Subject: [PATCH 57/59] forgot to swap names --- src/analysis/special_functions/arsinh.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 4b7e13d94cc38..377622f4d89cc 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -59,7 +59,7 @@ by rw [sinh_eq, arsinh, ← log_inv, exp_log (add_sqrt_one_add_pow_two_pos x), 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 +lemma sinh_surjective : function.surjective sinh := function.left_inverse.surjective sinh_arsinh /-- `sinh` is bijective, both injective and surjective. -/ lemma sinh_bijective : function.bijective sinh := @@ -77,4 +77,4 @@ end /-- `arsinh` is the left inverse of `sinh`. -/ lemma arsinh_sinh (x : ℝ) : arsinh (sinh x) = x := -function.right_inverse_of_injective_of_left_inverse sinh_injective arsinh_sinh x +function.right_inverse_of_injective_of_left_inverse sinh_injective sinh_arsinh x From 04ffedd737e479c14c2c99ec63f65c8b57c432ef Mon Sep 17 00:00:00 2001 From: James Arthur Date: Thu, 20 Aug 2020 10:05:12 +0100 Subject: [PATCH 58/59] Added `namespace real` and `@[pp_nodot]` --- src/analysis/special_functions/arsinh.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 377622f4d89cc..5c01e4fce7b17 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -4,8 +4,6 @@ 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 /-! @@ -26,9 +24,10 @@ inverse, arsinh. arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective -/ +namespace real /-- `arsinh` is defined using a logarithm, `arsinh x = log (x + sqrt(1 + x^2))`. -/ -def arsinh (x : ℝ) := log (x + sqrt (1 + x^2)) +@[pp_nodot] 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 @@ -78,3 +77,5 @@ end /-- `arsinh` is the left inverse of `sinh`. -/ lemma arsinh_sinh (x : ℝ) : arsinh (sinh x) = x := function.right_inverse_of_injective_of_left_inverse sinh_injective sinh_arsinh x + +end real From 694e47e933575d84322caa19967e64e45beae707 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 20 Aug 2020 14:17:19 +0200 Subject: [PATCH 59/59] Update src/analysis/special_functions/arsinh.lean --- src/analysis/special_functions/arsinh.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean index 5c01e4fce7b17..b043d9eb75610 100644 --- a/src/analysis/special_functions/arsinh.lean +++ b/src/analysis/special_functions/arsinh.lean @@ -64,7 +64,7 @@ lemma sinh_surjective : function.surjective sinh := function.left_inverse.surjec lemma sinh_bijective : function.bijective sinh := ⟨sinh_injective, sinh_surjective⟩ -/-- A rearrangment and `sqrt` of `real.cosh_sq_sub_sinh_sq`. -/ +/-- A rearrangement 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,