mathlib documentation

data.complex.exponential

Exponential, trigonometric and hyperbolic trigonometric functions

This file contains the definitions of the real and complex exponential, sine, cosine, tangent, hyperbolic sine, hypebolic cosine, and hyperbolic tangent functions.

source
theorem forall_ge_le_of_forall_le_succ {α : Type u_1} [preorder α] (f : ℕ → α) {m : ℕ} (h : ∀ (n : ℕ), n ≥ m → f n.succ ≤ f n) {l : ℕ} (k : ℕ) (H : k ≥ m) (a : k ≤ l) :
f l ≤ f k

source
theorem is_cau_of_decreasing_bounded {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ (n : ℕ), n ≥ m → abs (f n) ≤ a) (hnm : ∀ (n : ℕ), n ≥ m → f n.succ ≤ f n) :
is_cau_seq abs f

source
theorem is_cau_of_mono_bounded {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ (n : ℕ), n ≥ m → abs (f n) ≤ a) (hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f n.succ) :
is_cau_seq abs f

source
theorem is_cau_series_of_abv_le_cau {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] {abv : β → α} [is_absolute_value abv] {f : ℕ → β} {g : ℕ → α} (n : ℕ) (a : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m) (a_1 : is_cau_seq abs (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, g i)) :
is_cau_seq abv (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i)

source
theorem is_cau_series_of_abv_cau {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] {abv : β → α} [is_absolute_value abv] {f : ℕ → β} (a : is_cau_seq abs (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, abv (f n))) :
is_cau_seq abv (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, f n)

source
theorem is_cau_geo_series {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x : β) (hx1 : abv x < 1) :
is_cau_seq abv (λ (n : ℕ), ∑ (m : ℕ) in finset.range n, x ^ m)

source
theorem is_cau_geo_series_const {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (a : α) {x : α} (hx1 : abs x < 1) :
is_cau_seq abs (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, a * x ^ n)

source
theorem series_ratio_test {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] [archimedean α] {abv : β → α} [is_absolute_value abv] {f : ℕ → β} (n : ℕ) (r : α) (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) :
is_cau_seq abv (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, f n)

source
theorem sum_range_diag_flip {α : Type u_1} [add_comm_monoid α] (n : ℕ) (f : ℕ → ℕ → α) :
∑ (m : ℕ) in finset.range n, ∑ (k : ℕ) in finset.range (m + 1), f k (m - k) = ∑ (m : ℕ) in finset.range n, ∑ (k : ℕ) in finset.range (n - m), f m k

source
theorem sum_range_sub_sum_range {α : Type u_1} [add_comm_group α] {f : ℕ → α} {n m : ℕ} (hnm : n ≤ m) :
∑ (k : ℕ) in finset.range m, f k - ∑ (k : ℕ) in finset.range n, f k = ∑ (k : ℕ) in finset.filter (λ (k : ℕ), n ≤ k) (finset.range m), f k

source
theorem abv_sum_le_sum_abv {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] {abv : β → α} [is_absolute_value abv] {γ : Type u_3} (f : γ → β) (s : finset γ) :
abv (∑ (k : γ) in s, f k) ≤ ∑ (k : γ) in s, abv (f k)

source
theorem cauchy_product {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] {abv : β → α} [is_absolute_value abv] {a b : ℕ → β} (ha : is_cau_seq abs (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, abv (a n))) (hb : is_cau_seq abv (λ (m : ℕ), ∑ (n : ℕ) in finset.range m, b n)) (ε : α) (ε0 : 0 < ε) :
∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → abv ((∑ (k : ℕ) in finset.range j, a k) * ∑ (k : ℕ) in finset.range j, b k - ∑ (n : ℕ) in finset.range j, ∑ (m : ℕ) in finset.range (n + 1), (a m) * b (n - m)) < ε

source
theorem complex.is_cau_abs_exp (z : ℂ) :
is_cau_seq abs (λ (n : ℕ), ∑ (m : ℕ) in finset.range n, complex.abs (z ^ m / ↑(m.fact)))

source
theorem complex.is_cau_exp (z : ℂ) :
is_cau_seq complex.abs (λ (n : ℕ), ∑ (m : ℕ) in finset.range n, z ^ m / ↑(m.fact))

source
def complex.exp' (z : ℂ) :
cau_seq ℂ complex.abs

The Cauchy sequence consisting of partial sums of the Taylor series of the complex exponential function

Equations
source
def complex.exp (z : ℂ) :
ℂ

The complex exponential function, defined via its Taylor series

Equations
source
def complex.sin (z : ℂ) :
ℂ

The complex sine function, defined via exp

Equations
source
def complex.cos (z : ℂ) :
ℂ

The complex cosine function, defined via exp

Equations
source
def complex.tan (z : ℂ) :
ℂ

The complex tangent function, defined as sin z / cos z

Equations
source
def complex.sinh (z : ℂ) :
ℂ

The complex hyperbolic sine function, defined via exp

Equations
source
def complex.cosh (z : ℂ) :
ℂ

The complex hyperbolic cosine function, defined via exp

Equations
source
def complex.tanh (z : ℂ) :
ℂ

The complex hyperbolic tangent function, defined as sinh z / cosh z

Equations
source
def real.exp (x : ℝ) :
ℝ

The real exponential function, defined as the real part of the complex exponential

Equations
source
def real.sin (x : ℝ) :
ℝ

The real sine function, defined as the real part of the complex sine

Equations
source
def real.cos (x : ℝ) :
ℝ

The real cosine function, defined as the real part of the complex cosine

Equations
source
def real.tan (x : ℝ) :
ℝ

The real tangent function, defined as the real part of the complex tangent

Equations
source
def real.sinh (x : ℝ) :
ℝ

The real hypebolic sine function, defined as the real part of the complex hyperbolic sine

Equations
source
def real.cosh (x : ℝ) :
ℝ

The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine

Equations
source
def real.tanh (x : ℝ) :
ℝ

The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent

Equations
source
@[simp]
theorem complex.exp_zero  :
complex.exp 0 = 1

source
theorem complex.exp_add (x y : ℂ) :
complex.exp (x + y) = (complex.exp x) * complex.exp y

source
theorem complex.exp_list_sum (l : list ℂ) :
complex.exp l.sum = (list.map complex.exp l).prod

source
theorem complex.exp_multiset_sum (s : multiset ℂ) :
complex.exp s.sum = (multiset.map complex.exp s).prod

source
theorem complex.exp_sum {α : Type u_1} (s : finset α) (f : α → ℂ) :
complex.exp (∑ (x : α) in s, f x) = ∏ (x : α) in s, complex.exp (f x)

source
theorem complex.exp_nat_mul (x : ℂ) (n : ℕ) :
complex.exp ((↑n) * x) = complex.exp x ^ n

source
theorem complex.exp_ne_zero (x : ℂ) :
complex.exp x ≠ 0

source
theorem complex.exp_neg (x : ℂ) :
complex.exp (-x) = (complex.exp x)⁻¹

source
theorem complex.exp_sub (x y : ℂ) :
complex.exp (x - y) = complex.exp x / complex.exp y

source
@[simp]
theorem complex.exp_conj (x : ℂ) :
complex.exp (⇑complex.conj x) = ⇑complex.conj (complex.exp x)

source
@[simp]
theorem complex.of_real_exp_of_real_re (x : ℝ) :
↑((complex.exp ↑x).re) = complex.exp ↑x

source
@[simp]
theorem complex.of_real_exp (x : ℝ) :
↑(real.exp x) = complex.exp ↑x

source
@[simp]
theorem complex.exp_of_real_im (x : ℝ) :
(complex.exp ↑x).im = 0

source
theorem complex.exp_of_real_re (x : ℝ) :
(complex.exp ↑x).re = real.exp x

source
theorem complex.two_sinh (x : ℂ) :
2 * complex.sinh x = complex.exp x - complex.exp (-x)

source
theorem complex.two_cosh (x : ℂ) :
2 * complex.cosh x = complex.exp x + complex.exp (-x)

source
@[simp]
theorem complex.sinh_zero  :
complex.sinh 0 = 0

source
@[simp]
theorem complex.sinh_neg (x : ℂ) :
complex.sinh (-x) = -complex.sinh x

source
theorem complex.sinh_add (x y : ℂ) :
complex.sinh (x + y) = (complex.sinh x) * complex.cosh y + (complex.cosh x) * complex.sinh y

source
@[simp]
theorem complex.cosh_zero  :
complex.cosh 0 = 1

source
@[simp]
theorem complex.cosh_neg (x : ℂ) :
complex.cosh (-x) = complex.cosh x

source
theorem complex.cosh_add (x y : ℂ) :
complex.cosh (x + y) = (complex.cosh x) * complex.cosh y + (complex.sinh x) * complex.sinh y

source
theorem complex.sinh_sub (x y : ℂ) :
complex.sinh (x - y) = (complex.sinh x) * complex.cosh y - (complex.cosh x) * complex.sinh y

source
theorem complex.cosh_sub (x y : ℂ) :
complex.cosh (x - y) = (complex.cosh x) * complex.cosh y - (complex.sinh x) * complex.sinh y

source
theorem complex.sinh_conj (x : ℂ) :
complex.sinh (⇑complex.conj x) = ⇑complex.conj (complex.sinh x)

source
@[simp]
theorem complex.of_real_sinh_of_real_re (x : ℝ) :
↑((complex.sinh ↑x).re) = complex.sinh ↑x

source
@[simp]
theorem complex.of_real_sinh (x : ℝ) :
↑(real.sinh x) = complex.sinh ↑x

source
@[simp]
theorem complex.sinh_of_real_im (x : ℝ) :
(complex.sinh ↑x).im = 0

source
theorem complex.sinh_of_real_re (x : ℝ) :
(complex.sinh ↑x).re = real.sinh x

source
theorem complex.cosh_conj (x : ℂ) :
complex.cosh (⇑complex.conj x) = ⇑complex.conj (complex.cosh x)

source
@[simp]
theorem complex.of_real_cosh_of_real_re (x : ℝ) :
↑((complex.cosh ↑x).re) = complex.cosh ↑x

source
@[simp]
theorem complex.of_real_cosh (x : ℝ) :
↑(real.cosh x) = complex.cosh ↑x

source
@[simp]
theorem complex.cosh_of_real_im (x : ℝ) :
(complex.cosh ↑x).im = 0

source
theorem complex.cosh_of_real_re (x : ℝ) :
(complex.cosh ↑x).re = real.cosh x

source
theorem complex.tanh_eq_sinh_div_cosh (x : ℂ) :
complex.tanh x = complex.sinh x / complex.cosh x

source
@[simp]
theorem complex.tanh_zero  :
complex.tanh 0 = 0

source
@[simp]
theorem complex.tanh_neg (x : ℂ) :
complex.tanh (-x) = -complex.tanh x

source
theorem complex.tanh_conj (x : ℂ) :
complex.tanh (⇑complex.conj x) = ⇑complex.conj (complex.tanh x)

source
@[simp]
theorem complex.of_real_tanh_of_real_re (x : ℝ) :
↑((complex.tanh ↑x).re) = complex.tanh ↑x

source
@[simp]
theorem complex.of_real_tanh (x : ℝ) :
↑(real.tanh x) = complex.tanh ↑x

source
@[simp]
theorem complex.tanh_of_real_im (x : ℝ) :
(complex.tanh ↑x).im = 0

source
theorem complex.tanh_of_real_re (x : ℝ) :
(complex.tanh ↑x).re = real.tanh x

source
theorem complex.cosh_add_sinh (x : ℂ) :
complex.cosh x + complex.sinh x = complex.exp x

source
theorem complex.sinh_add_cosh (x : ℂ) :
complex.sinh x + complex.cosh x = complex.exp x

source
theorem complex.cosh_sub_sinh (x : ℂ) :
complex.cosh x - complex.sinh x = complex.exp (-x)

source
theorem complex.cosh_sq_sub_sinh_sq (x : ℂ) :
complex.cosh x ^ 2 - complex.sinh x ^ 2 = 1

source
@[simp]
theorem complex.sin_zero  :
complex.sin 0 = 0

source
@[simp]
theorem complex.sin_neg (x : ℂ) :
complex.sin (-x) = -complex.sin x

source
theorem complex.two_sin (x : ℂ) :
2 * complex.sin x = (complex.exp ((-x) * complex.I) - complex.exp (x * complex.I)) * complex.I

source
theorem complex.two_cos (x : ℂ) :
2 * complex.cos x = complex.exp (x * complex.I) + complex.exp ((-x) * complex.I)

source
theorem complex.sinh_mul_I (x : ℂ) :
complex.sinh (x * complex.I) = (complex.sin x) * complex.I

source
theorem complex.cosh_mul_I (x : ℂ) :
complex.cosh (x * complex.I) = complex.cos x

source
theorem complex.sin_add (x y : ℂ) :
complex.sin (x + y) = (complex.sin x) * complex.cos y + (complex.cos x) * complex.sin y

source
@[simp]
theorem complex.cos_zero  :
complex.cos 0 = 1

source
@[simp]
theorem complex.cos_neg (x : ℂ) :
complex.cos (-x) = complex.cos x

source
theorem complex.cos_add (x y : ℂ) :
complex.cos (x + y) = (complex.cos x) * complex.cos y - (complex.sin x) * complex.sin y

source
theorem complex.sin_sub (x y : ℂ) :
complex.sin (x - y) = (complex.sin x) * complex.cos y - (complex.cos x) * complex.sin y

source
theorem complex.cos_sub (x y : ℂ) :
complex.cos (x - y) = (complex.cos x) * complex.cos y + (complex.sin x) * complex.sin y

source
theorem complex.sin_conj (x : ℂ) :
complex.sin (⇑complex.conj x) = ⇑complex.conj (complex.sin x)

source
@[simp]
theorem complex.of_real_sin_of_real_re (x : ℝ) :
↑((complex.sin ↑x).re) = complex.sin ↑x

source
@[simp]
theorem complex.of_real_sin (x : ℝ) :
↑(real.sin x) = complex.sin ↑x

source
@[simp]
theorem complex.sin_of_real_im (x : ℝ) :
(complex.sin ↑x).im = 0

source
theorem complex.sin_of_real_re (x : ℝ) :
(complex.sin ↑x).re = real.sin x

source
theorem complex.cos_conj (x : ℂ) :
complex.cos (⇑complex.conj x) = ⇑complex.conj (complex.cos x)

source
@[simp]
theorem complex.of_real_cos_of_real_re (x : ℝ) :
↑((complex.cos ↑x).re) = complex.cos ↑x

source
@[simp]
theorem complex.of_real_cos (x : ℝ) :
↑(real.cos x) = complex.cos ↑x

source
@[simp]
theorem complex.cos_of_real_im (x : ℝ) :
(complex.cos ↑x).im = 0

source
theorem complex.cos_of_real_re (x : ℝ) :
(complex.cos ↑x).re = real.cos x

source
@[simp]
theorem complex.tan_zero  :
complex.tan 0 = 0

source
theorem complex.tan_eq_sin_div_cos (x : ℂ) :
complex.tan x = complex.sin x / complex.cos x

source
@[simp]
theorem complex.tan_neg (x : ℂ) :
complex.tan (-x) = -complex.tan x

source
theorem complex.tan_conj (x : ℂ) :
complex.tan (⇑complex.conj x) = ⇑complex.conj (complex.tan x)

source
@[simp]
theorem complex.of_real_tan_of_real_re (x : ℝ) :
↑((complex.tan ↑x).re) = complex.tan ↑x

source
@[simp]
theorem complex.of_real_tan (x : ℝ) :
↑(real.tan x) = complex.tan ↑x

source
@[simp]
theorem complex.tan_of_real_im (x : ℝ) :
(complex.tan ↑x).im = 0

source
theorem complex.tan_of_real_re (x : ℝ) :
(complex.tan ↑x).re = real.tan x

source
theorem complex.cos_add_sin_I (x : ℂ) :
complex.cos x + (complex.sin x) * complex.I = complex.exp (x * complex.I)

source
theorem complex.cos_sub_sin_I (x : ℂ) :
complex.cos x - (complex.sin x) * complex.I = complex.exp ((-x) * complex.I)

source
theorem complex.sin_sq_add_cos_sq (x : ℂ) :
complex.sin x ^ 2 + complex.cos x ^ 2 = 1

source
theorem complex.cos_two_mul' (x : ℂ) :
complex.cos (2 * x) = complex.cos x ^ 2 - complex.sin x ^ 2

source
theorem complex.cos_two_mul (x : ℂ) :
complex.cos (2 * x) = 2 * complex.cos x ^ 2 - 1

source
theorem complex.sin_two_mul (x : ℂ) :
complex.sin (2 * x) = (2 * complex.sin x) * complex.cos x

source
theorem complex.cos_square (x : ℂ) :
complex.cos x ^ 2 = 1 / 2 + complex.cos (2 * x) / 2

source
theorem complex.sin_square (x : ℂ) :
complex.sin x ^ 2 = 1 - complex.cos x ^ 2

source
theorem complex.exp_mul_I (x : ℂ) :
complex.exp (x * complex.I) = complex.cos x + (complex.sin x) * complex.I

source
theorem complex.exp_add_mul_I (x y : ℂ) :
complex.exp (x + y * complex.I) = (complex.exp x) * (complex.cos y + (complex.sin y) * complex.I)

source
theorem complex.exp_eq_exp_re_mul_sin_add_cos (x : ℂ) :
complex.exp x = (complex.exp ↑(x.re)) * (complex.cos ↑(x.im) + (complex.sin ↑(x.im)) * complex.I)

source
theorem complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
(complex.cos z + (complex.sin z) * complex.I) ^ n = complex.cos ((↑n) * z) + (complex.sin ((↑n) * z)) * complex.I

De Moivre's formula

source
@[simp]
theorem real.exp_zero  :
real.exp 0 = 1

source
theorem real.exp_add (x y : ℝ) :
real.exp (x + y) = (real.exp x) * real.exp y

source
theorem real.exp_list_sum (l : list ℝ) :
real.exp l.sum = (list.map real.exp l).prod

source
theorem real.exp_multiset_sum (s : multiset ℝ) :
real.exp s.sum = (multiset.map real.exp s).prod

source
theorem real.exp_sum {α : Type u_1} (s : finset α) (f : α → ℝ) :
real.exp (∑ (x : α) in s, f x) = ∏ (x : α) in s, real.exp (f x)

source
theorem real.exp_nat_mul (x : ℝ) (n : ℕ) :
real.exp ((↑n) * x) = real.exp x ^ n

source
theorem real.exp_ne_zero (x : ℝ) :
real.exp x ≠ 0

source
theorem real.exp_neg (x : ℝ) :
real.exp (-x) = (real.exp x)⁻¹

source
theorem real.exp_sub (x y : ℝ) :
real.exp (x - y) = real.exp x / real.exp y

source
@[simp]
theorem real.sin_zero  :
real.sin 0 = 0

source
@[simp]
theorem real.sin_neg (x : ℝ) :
real.sin (-x) = -real.sin x

source
theorem real.sin_add (x y : ℝ) :
real.sin (x + y) = (real.sin x) * real.cos y + (real.cos x) * real.sin y

source
@[simp]
theorem real.cos_zero  :
real.cos 0 = 1

source
@[simp]
theorem real.cos_neg (x : ℝ) :
real.cos (-x) = real.cos x

source
theorem real.cos_add (x y : ℝ) :
real.cos (x + y) = (real.cos x) * real.cos y - (real.sin x) * real.sin y

source
theorem real.sin_sub (x y : ℝ) :
real.sin (x - y) = (real.sin x) * real.cos y - (real.cos x) * real.sin y

source
theorem real.cos_sub (x y : ℝ) :
real.cos (x - y) = (real.cos x) * real.cos y + (real.sin x) * real.sin y

source
theorem real.tan_eq_sin_div_cos (x : ℝ) :
real.tan x = real.sin x / real.cos x

source
@[simp]
theorem real.tan_zero  :
real.tan 0 = 0

source
@[simp]
theorem real.tan_neg (x : ℝ) :
real.tan (-x) = -real.tan x

source
theorem real.sin_sq_add_cos_sq (x : ℝ) :
real.sin x ^ 2 + real.cos x ^ 2 = 1

source
theorem real.sin_sq_le_one (x : ℝ) :
real.sin x ^ 2 ≤ 1

source
theorem real.cos_sq_le_one (x : ℝ) :
real.cos x ^ 2 ≤ 1

source
theorem real.abs_sin_le_one (x : ℝ) :
abs (real.sin x) ≤ 1

source
theorem real.abs_cos_le_one (x : ℝ) :
abs (real.cos x) ≤ 1

source
theorem real.sin_le_one (x : ℝ) :
real.sin x ≤ 1

source
theorem real.cos_le_one (x : ℝ) :
real.cos x ≤ 1

source
theorem real.neg_one_le_sin (x : ℝ) :
-1 ≤ real.sin x

source
theorem real.neg_one_le_cos (x : ℝ) :
-1 ≤ real.cos x

source
theorem real.cos_two_mul (x : ℝ) :
real.cos (2 * x) = 2 * real.cos x ^ 2 - 1

source
theorem real.sin_two_mul (x : ℝ) :
real.sin (2 * x) = (2 * real.sin x) * real.cos x

source
theorem real.cos_square (x : ℝ) :
real.cos x ^ 2 = 1 / 2 + real.cos (2 * x) / 2

source
theorem real.sin_square (x : ℝ) :
real.sin x ^ 2 = 1 - real.cos x ^ 2

source
theorem real.sinh_eq (x : ℝ) :
real.sinh x = (real.exp x - real.exp (-x)) / 2

The definition of sinh in terms of exp.

source
@[simp]
theorem real.sinh_zero  :
real.sinh 0 = 0

source
@[simp]
theorem real.sinh_neg (x : ℝ) :
real.sinh (-x) = -real.sinh x

source
theorem real.sinh_add (x y : ℝ) :
real.sinh (x + y) = (real.sinh x) * real.cosh y + (real.cosh x) * real.sinh y

source
theorem real.cosh_eq (x : ℝ) :
real.cosh x = (real.exp x + real.exp (-x)) / 2

The definition of cosh in terms of exp.

source
@[simp]
theorem real.cosh_zero  :
real.cosh 0 = 1

source
@[simp]
theorem real.cosh_neg (x : ℝ) :
real.cosh (-x) = real.cosh x

source
theorem real.cosh_add (x y : ℝ) :
real.cosh (x + y) = (real.cosh x) * real.cosh y + (real.sinh x) * real.sinh y

source
theorem real.sinh_sub (x y : ℝ) :
real.sinh (x - y) = (real.sinh x) * real.cosh y - (real.cosh x) * real.sinh y

source
theorem real.cosh_sub (x y : ℝ) :
real.cosh (x - y) = (real.cosh x) * real.cosh y - (real.sinh x) * real.sinh y

source
theorem real.cosh_sq_sub_sinh_sq (x : ℝ) :
real.cosh x ^ 2 - real.sinh x ^ 2 = 1

source
theorem real.tanh_eq_sinh_div_cosh (x : ℝ) :
real.tanh x = real.sinh x / real.cosh x

source
@[simp]
theorem real.tanh_zero  :
real.tanh 0 = 0

source
@[simp]
theorem real.tanh_neg (x : ℝ) :
real.tanh (-x) = -real.tanh x

source
theorem real.add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
x + 1 ≤ real.exp x

source
theorem real.one_le_exp {x : ℝ} (hx : 0 ≤ x) :
1 ≤ real.exp x

source
theorem real.exp_pos (x : ℝ) :
0 < real.exp x

source
@[simp]
theorem real.abs_exp (x : ℝ) :
abs (real.exp x) = real.exp x

source
theorem real.exp_strict_mono  :
strict_mono real.exp

source
theorem real.exp_monotone {x y : ℝ} (a : x ≤ y) :
real.exp x ≤ real.exp y

source
theorem real.exp_lt_exp {x y : ℝ} :
real.exp x < real.exp y ↔ x < y

source
theorem real.exp_le_exp {x y : ℝ} :
real.exp x ≤ real.exp y ↔ x ≤ y

source
theorem real.exp_injective  :
function.injective real.exp

source
@[simp]
theorem real.exp_eq_one_iff (x : ℝ) :
real.exp x = 1 ↔ x = 0

source
theorem real.one_lt_exp_iff {x : ℝ} :
1 < real.exp x ↔ 0 < x

source
theorem real.exp_lt_one_iff {x : ℝ} :
real.exp x < 1 ↔ x < 0

source
theorem real.cosh_pos (x : ℝ) :
0 < real.cosh x

real.cosh is always positive

source
theorem complex.sum_div_fact_le {α : Type u_1} [discrete_linear_ordered_field α] (n j : ℕ) (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (k : ℕ), n ≤ k) (finset.range j), 1 / ↑(m.fact) ≤ (↑(n.succ)) * ((↑(n.fact)) * ↑n)⁻¹

source
theorem complex.exp_bound {x : ℂ} (hx : complex.abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
complex.abs (complex.exp x - ∑ (m : ℕ) in finset.range n, x ^ m / ↑(m.fact)) ≤ (complex.abs x ^ n) * (↑(n.succ)) * ((↑(n.fact)) * ↑n)⁻¹

source
theorem complex.abs_exp_sub_one_le {x : ℂ} (hx : complex.abs x ≤ 1) :
complex.abs (complex.exp x - 1) ≤ 2 * complex.abs x

source
theorem complex.abs_exp_sub_one_sub_id_le {x : ℂ} (hx : complex.abs x ≤ 1) :
complex.abs (complex.exp x - 1 - x) ≤ complex.abs x ^ 2

source
theorem real.cos_bound {x : ℝ} (hx : abs x ≤ 1) :
abs (real.cos x - (1 - x ^ 2 / 2)) ≤ (abs x ^ 4) * (5 / 96)

source
theorem real.sin_bound {x : ℝ} (hx : abs x ≤ 1) :
abs (real.sin x - (x - x ^ 3 / 6)) ≤ (abs x ^ 4) * (5 / 96)

source
theorem real.cos_pos_of_le_one {x : ℝ} (hx : abs x ≤ 1) :
0 < real.cos x

source
theorem real.sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) :
0 < real.sin x

source
theorem real.sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) :
0 < real.sin x

source
theorem real.cos_one_le  :
real.cos 1 ≤ 2 / 3

source
theorem real.cos_one_pos  :
0 < real.cos 1

source
theorem real.cos_two_neg  :
real.cos 2 < 0

source
theorem complex.abs_cos_add_sin_mul_I (x : ℝ) :
complex.abs (complex.cos ↑x + (complex.sin ↑x) * complex.I) = 1

source
theorem complex.abs_exp_eq_iff_re_eq {x y : ℂ} :
complex.abs (complex.exp x) = complex.abs (complex.exp y) ↔ x.re = y.re

source
@[simp]
theorem complex.abs_exp_of_real (x : ℝ) :
complex.abs (complex.exp ↑x) = real.exp x