Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(analysis/special_functions/arsinh): inverse hyperbolic sine func…
…tion (#3801) Added the following lemmas and definitions: `cosh_def` `sinh_def` `cosh_pos` `sinh_strict_mono` `sinh_injective` `sinh_surjective` `sinh_bijective` `real.cosh_sq_sub_sinh_sq` `sqrt_one_add_sinh_sq` `sinh_arsinh` `arsinh_sin` This is from the list of UG not in lean. `cosh` coming soon.
- Loading branch information
1 parent
7a48761
commit 4921be9
Showing
4 changed files
with
110 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,81 @@ | ||
/- | ||
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 | ||
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 | ||
-/ | ||
|
||
namespace real | ||
|
||
/-- `arsinh` is defined using a logarithm, `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 | ||
|
||
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 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, | ||
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 sinh_arsinh | ||
|
||
/-- `sinh` is bijective, both injective and surjective. -/ | ||
lemma sinh_bijective : function.bijective sinh := | ||
⟨sinh_injective, sinh_surjective⟩ | ||
|
||
/-- 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, | ||
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 arsinh_sinh (x : ℝ) : arsinh (sinh x) = x := | ||
function.right_inverse_of_injective_of_left_inverse sinh_injective sinh_arsinh x | ||
|
||
end real |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters