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 : ) (H : k m) :
k lf l f k
theorem is_cau_of_decreasing_bounded {α : Type u_1} [linear_ordered_field α] [archimedean α] (f : → α) {a : α} {m : } (ham : ∀ (n : ), n mabs (f n) a) (hnm : ∀ (n : ), n mf n.succ f n) :
theorem is_cau_of_mono_bounded {α : Type u_1} [linear_ordered_field α] [archimedean α] (f : → α) {a : α} {m : } (ham : ∀ (n : ), n mabs (f n) a) (hnm : ∀ (n : ), n mf n f n.succ) :
theorem is_cau_series_of_abv_le_cau {α : Type u_1} {β : Type u_2} [ring β] [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 β] [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} [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)
theorem is_cau_geo_series_const {α : Type u_1} [linear_ordered_field α] [archimedean α] (a : α) {x : α} (hx1 : abs x < 1) :
is_cau_seq abs (λ (m : ), ∑ (n : ) in finset.range m, a * x ^ n)
theorem series_ratio_test {α : Type u_1} {β : Type u_2} [ring β] [linear_ordered_field α] [archimedean α] {abv : β → α} [is_absolute_value abv] {f : → β} (n : ) (r : α) (hr0 : 0 r) (hr1 : r < 1) (h : ∀ (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 : } (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
theorem abv_sum_le_sum_abv {α : Type u_1} {β : Type u_2} [ring β] [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 β] [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 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 (z : ) :

The complex exponential function, defined via its Taylor series

Equations
def complex.sin (z : ) :

The complex sine function, defined via exp

Equations
def complex.cos (z : ) :

The complex cosine function, defined via exp

Equations
def complex.tan (z : ) :

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

Equations
def complex.sinh (z : ) :

The complex hyperbolic sine function, defined via exp

Equations
def complex.cosh (z : ) :

The complex hyperbolic cosine function, defined via exp

Equations
def complex.tanh (z : ) :

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

Equations
def real.exp (x : ) :

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

Equations
def real.sin (x : ) :

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

Equations
def real.cos (x : ) :

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

Equations
def real.tan (x : ) :

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

Equations
def real.sinh (x : ) :

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

Equations
def real.cosh (x : ) :

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

Equations
def real.tanh (x : ) :

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 : ) :
@[simp]
theorem complex.sin_sq_add_cos_sq (x : ) :
@[simp]
theorem complex.cos_sq_add_sin_sq (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 : ) :
theorem complex.exp_re (x : ) :
theorem complex.exp_im (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)
theorem real.tan_mul_cos {x : } (hx : real.cos x 0) :
@[simp]
theorem real.tan_zero  :
@[simp]
theorem real.tan_neg (x : ) :
@[simp]
theorem real.sin_sq_add_cos_sq (x : ) :
real.sin x ^ 2 + real.cos x ^ 2 = 1
@[simp]
theorem real.cos_sq_add_sin_sq (x : ) :
real.cos x ^ 2 + real.sin 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.inv_one_add_tan_sq {x : } (hx : real.cos x 0) :
(1 + real.tan x ^ 2)⁻¹ = real.cos x ^ 2
theorem real.tan_sq_div_one_add_tan_sq {x : } (hx : real.cos x 0) :
real.tan x ^ 2 / (1 + real.tan x ^ 2) = real.sin 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 : } (hx : 0 x) :
x + 1 real.exp x
theorem real.one_le_exp {x : } (hx : 0 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
@[simp]
theorem real.exp_lt_exp {x y : } :
@[simp]
theorem real.exp_le_exp {x y : } :
@[simp]
theorem real.exp_eq_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} [linear_ordered_field α] (n j : ) (hn : 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 : } (hn : 0 < n) :
complex.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 : } (hn : 0 < n) :
abs (real.exp x - ∑ (m : ) in finset.range n, x ^ m / m!) (abs x ^ n) * ((n.succ) / (n!) * n)
def real.exp_near (n : ) (x r : ) :

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 : ) (e₁ : n + 1 = m) (h : abs x 1) :
abs (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₂ : ) (e : abs (1 + (x / m) * a₂ - a₁) b₁ - (abs x / m) * b₂) (h : 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 : ) (er : m = rm) (h : abs x 1) (e : abs (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 : } (er : m = rm) (h : abs (real.exp 1 - real.exp_near m 1 ((a₁ - 1) * rm)) (abs 1 ^ m / m!) * b₁ * rm) :
abs (real.exp 1 - real.exp_near n 1 a₁) (abs 1 ^ n / n!) * b₁
theorem real.exp_approx_start (x a b : ) (h : abs (real.exp x - real.exp_near 0 x a) (abs x ^ 0 / 0!) * b) :
abs (real.exp x - a) b
theorem real.cos_bound {x : } (hx : abs x 1) :
abs (real.cos x - (1 - x ^ 2 / 2)) (abs x ^ 4) * (5 / 96)
theorem real.sin_bound {x : } (hx : abs x 1) :
abs (real.sin x - (x - x ^ 3 / 6)) (abs x ^ 4) * (5 / 96)
theorem real.cos_pos_of_le_one {x : } (hx : abs x 1) :
theorem real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
theorem real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
theorem real.cos_one_le  :
real.cos 1 2 / 3
theorem real.cos_one_pos  :
theorem real.cos_two_neg  :