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, hyperbolic cosine, and hyperbolic tangent functions.

theorem forall_ge_le_of_forall_le_succ {α : Type u_1} [preorder α] (f : → α) {m : } (h : ∀ (n : ), n mf n.succ f n) {l : } (k : ) :
k mk lf l f k

theorem is_cau_of_decreasing_bounded {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (f : → α) {a : α} {m : } :
(∀ (n : ), n mabs (f n) a)(∀ (n : ), n mf n.succ f n)is_cau_seq abs f

theorem is_cau_of_mono_bounded {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (f : → α) {a : α} {m : } :
(∀ (n : ), n mabs (f n) a)(∀ (n : ), n mf n f n.succ)is_cau_seq abs f

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 : ) :
(∀ (m : ), n mabv (f m) g m)is_cau_seq abs (λ (n : ), ∑ (i : ) in finset.range n, g i)is_cau_seq abv (λ (n : ), ∑ (i : ) in finset.range n, f i)

theorem is_cau_series_of_abv_cau {α : Type u_1} {β : Type u_2} [ring β] [discrete_linear_ordered_field α] {abv : β → α} [is_absolute_value abv] {f : → β} :
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)

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

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

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

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

theorem sum_range_sub_sum_range {α : Type u_1} [add_comm_group α] {f : → α} {n m : } :
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

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)

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 < ε(∃ (i : ), ∀ (j : ), j iabv ((∑ (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)) < ε)

theorem complex.is_cau_abs_exp (z : ) :
is_cau_seq abs (λ (n : ), ∑ (m : ) in finset.range n, complex.abs (z ^ m / m!))

theorem complex.is_cau_exp (z : ) :
is_cau_seq complex.abs (λ (n : ), ∑ (m : ) in finset.range n, z ^ m / m!)

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

Equations
def complex.exp  :

The complex exponential function, defined via its Taylor series

Equations
def complex.sin  :

The complex sine function, defined via exp

Equations
def complex.cos  :

The complex cosine function, defined via exp

Equations
def complex.tan  :

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

Equations
def complex.sinh  :

The complex hyperbolic sine function, defined via exp

Equations
def complex.cosh  :

The complex hyperbolic cosine function, defined via exp

Equations
def complex.tanh  :

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

Equations
def real.exp  :

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

Equations
def real.sin  :

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

Equations
def real.cos  :

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

Equations
def real.tan  :

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

Equations
def real.sinh  :

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

Equations
def real.cosh  :

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

Equations
def real.tanh  :

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

Equations
@[simp]
theorem complex.exp_zero  :

theorem complex.exp_add (x y : ) :

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

theorem complex.exp_nat_mul (x : ) (n : ) :

@[simp]

@[simp]
theorem complex.exp_of_real_im (x : ) :

@[simp]
theorem complex.sinh_zero  :

@[simp]

@[simp]
theorem complex.cosh_zero  :

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]
theorem complex.tanh_zero  :

@[simp]

@[simp]

@[simp]

@[simp]
theorem complex.sin_zero  :

@[simp]
theorem complex.sin_neg (x : ) :

@[simp]
theorem complex.cos_zero  :

@[simp]
theorem complex.cos_neg (x : ) :

theorem complex.sin_sub_sin (x y : ) :
complex.sin x - complex.sin y = (2 * complex.sin ((x - y) / 2)) * complex.cos ((x + y) / 2)

theorem complex.cos_sub_cos (x y : ) :
complex.cos x - complex.cos y = ((-2) * complex.sin ((x + y) / 2)) * complex.sin ((x - y) / 2)

theorem complex.cos_add_cos (x y : ) :
complex.cos x + complex.cos y = (2 * complex.cos ((x + y) / 2)) * complex.cos ((x - y) / 2)

@[simp]

@[simp]
theorem complex.sin_of_real_im (x : ) :

@[simp]

@[simp]
theorem complex.cos_of_real_im (x : ) :

@[simp]
theorem complex.tan_zero  :

@[simp]
theorem complex.tan_neg (x : ) :

@[simp]

@[simp]
theorem complex.tan_of_real_im (x : ) :

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

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

theorem complex.cos_square' (x : ) :

theorem complex.sin_square (x : ) :

theorem complex.cos_three_mul (x : ) :

theorem complex.sin_three_mul (x : ) :

De Moivre's formula

@[simp]
theorem real.exp_zero  :

theorem real.exp_add (x y : ) :

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

theorem real.exp_nat_mul (x : ) (n : ) :
real.exp ((n) * x) = real.exp x ^ n

theorem real.exp_ne_zero (x : ) :

theorem real.exp_neg (x : ) :

theorem real.exp_sub (x y : ) :

@[simp]
theorem real.sin_zero  :

@[simp]
theorem real.sin_neg (x : ) :

theorem real.sin_add (x y : ) :

@[simp]
theorem real.cos_zero  :

@[simp]
theorem real.cos_neg (x : ) :

theorem real.cos_add (x y : ) :

theorem real.sin_sub (x y : ) :

theorem real.cos_sub (x y : ) :

theorem real.sin_sub_sin (x y : ) :
real.sin x - real.sin y = (2 * real.sin ((x - y) / 2)) * real.cos ((x + y) / 2)

theorem real.cos_sub_cos (x y : ) :
real.cos x - real.cos y = ((-2) * real.sin ((x + y) / 2)) * real.sin ((x - y) / 2)

theorem real.cos_add_cos (x y : ) :
real.cos x + real.cos y = (2 * real.cos ((x + y) / 2)) * real.cos ((x - y) / 2)

@[simp]
theorem real.tan_zero  :

@[simp]
theorem real.tan_neg (x : ) :

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

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

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

theorem real.abs_sin_le_one (x : ) :

theorem real.abs_cos_le_one (x : ) :

theorem real.sin_le_one (x : ) :

theorem real.cos_le_one (x : ) :

theorem real.neg_one_le_sin (x : ) :

theorem real.neg_one_le_cos (x : ) :

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

theorem real.cos_two_mul' (x : ) :
real.cos (2 * x) = real.cos x ^ 2 - real.sin x ^ 2

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

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

theorem real.cos_square' (x : ) :
real.cos x ^ 2 = 1 - real.sin x ^ 2

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

theorem real.cos_three_mul (x : ) :
real.cos (3 * x) = 4 * real.cos x ^ 3 - 3 * real.cos x

theorem real.sin_three_mul (x : ) :
real.sin (3 * x) = 3 * real.sin x - 4 * real.sin x ^ 3

theorem real.sinh_eq (x : ) :

The definition of sinh in terms of exp.

@[simp]
theorem real.sinh_zero  :

@[simp]
theorem real.sinh_neg (x : ) :

theorem real.sinh_add (x y : ) :

theorem real.cosh_eq (x : ) :

The definition of cosh in terms of exp.

@[simp]
theorem real.cosh_zero  :

@[simp]
theorem real.cosh_neg (x : ) :

theorem real.cosh_add (x y : ) :

theorem real.sinh_sub (x y : ) :

theorem real.cosh_sub (x y : ) :

@[simp]
theorem real.tanh_zero  :

@[simp]
theorem real.tanh_neg (x : ) :

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

theorem real.cosh_square (x : ) :
real.cosh x ^ 2 = real.sinh x ^ 2 + 1

theorem real.sinh_square (x : ) :
real.sinh x ^ 2 = real.cosh x ^ 2 - 1

theorem real.cosh_two_mul (x : ) :

theorem real.sinh_two_mul (x : ) :

theorem real.cosh_three_mul (x : ) :
real.cosh (3 * x) = 4 * real.cosh x ^ 3 - 3 * real.cosh x

theorem real.sinh_three_mul (x : ) :
real.sinh (3 * x) = 4 * real.sinh x ^ 3 + 3 * real.sinh x

theorem real.add_one_le_exp_of_nonneg {x : } :
0 xx + 1 real.exp x

theorem real.one_le_exp {x : } :
0 x1 real.exp x

theorem real.exp_pos (x : ) :

@[simp]
theorem real.abs_exp (x : ) :

theorem real.exp_monotone {x y : } :
x yreal.exp x real.exp y

theorem real.exp_lt_exp {x y : } :

theorem real.exp_le_exp {x y : } :

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

@[simp]
theorem real.one_lt_exp_iff {x : } :
1 < real.exp x 0 < x

@[simp]
theorem real.exp_lt_one_iff {x : } :
real.exp x < 1 x < 0

@[simp]
theorem real.exp_le_one_iff {x : } :

@[simp]
theorem real.one_le_exp_iff {x : } :

theorem real.cosh_pos (x : ) :

real.cosh is always positive

theorem complex.sum_div_factorial_le {α : Type u_1} [discrete_linear_ordered_field α] (n j : ) :
0 < n∑ (m : ) in finset.filter (λ (k : ), n k) (finset.range j), 1 / m! ((n.succ)) * ((n!) * n)⁻¹

theorem complex.exp_bound {x : } (hx : complex.abs x 1) {n : } :
0 < ncomplex.abs (complex.exp x - ∑ (m : ) in finset.range n, x ^ m / m!) (complex.abs x ^ n) * ((n.succ)) * ((n!) * n)⁻¹

theorem real.exp_bound {x : } (hx : abs x 1) {n : } :
0 < nabs (real.exp x - ∑ (m : ) in finset.range n, x ^ m / m!) (abs x ^ n) * ((n.succ) / (n!) * n)

def real.exp_near  :

A finite initial segment of the exponential series, followed by an arbitrary tail. For fixed n this is just a linear map wrt r, and each map is a simple linear function of the previous (see exp_near_succ), with exp_near n x r ⟶ exp x as n ⟶ ∞, for any r.

Equations
@[simp]
theorem real.exp_near_zero (x r : ) :

@[simp]
theorem real.exp_near_succ (n : ) (x r : ) :
real.exp_near (n + 1) x r = real.exp_near n x (1 + (x / (n + 1)) * r)

theorem real.exp_near_sub (n : ) (x r₁ r₂ : ) :
real.exp_near n x r₁ - real.exp_near n x r₂ = (x ^ n / n!) * (r₁ - r₂)

theorem real.exp_approx_end (n m : ) (x : ) :
n + 1 = mabs x 1abs (real.exp x - real.exp_near m x 0) (abs x ^ m / m!) * ((m + 1) / m)

theorem real.exp_approx_succ {n : } {x a₁ b₁ : } (m : ) (e₁ : n + 1 = m) (a₂ b₂ : ) :
abs (1 + (x / m) * a₂ - a₁) b₁ - (abs x / m) * b₂abs (real.exp x - real.exp_near m x a₂) (abs x ^ m / m!) * b₂abs (real.exp x - real.exp_near n x a₁) (abs x ^ n / n!) * b₁

theorem real.exp_approx_end' {n : } {x a b : } (m : ) (e₁ : n + 1 = m) (rm : ) :
m = rmabs x 1abs (1 - a) b - (abs x / rm) * ((rm + 1) / rm)abs (real.exp x - real.exp_near n x a) (abs x ^ n / n!) * b

theorem real.exp_1_approx_succ_eq {n : } {a₁ b₁ : } {m : } (en : n + 1 = m) {rm : } :
m = rmabs (real.exp 1 - real.exp_near m 1 ((a₁ - 1) * rm)) (abs 1 ^ m / m!) * b₁ * rmabs (real.exp 1 - real.exp_near n 1 a₁) (abs 1 ^ n / n!) * b₁

theorem real.exp_approx_start (x a b : ) :
abs (real.exp x - real.exp_near 0 x a) (abs x ^ 0 / 0!) * babs (real.exp x - a) b

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

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

theorem real.cos_pos_of_le_one {x : } :
abs x 10 < real.cos x

theorem real.sin_pos_of_pos_of_le_one {x : } :
0 < xx 10 < real.sin x

theorem real.sin_pos_of_pos_of_le_two {x : } :
0 < xx 20 < real.sin x

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

theorem real.cos_one_pos  :

theorem real.cos_two_neg  :