mathlib3 documentation

data.complex.exponential

Exponential, trigonometric and hyperbolic trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem is_cau_of_decreasing_bounded {α : Type u_1} [linear_ordered_field α] [archimedean α] (f : α) {a : α} {m : } (ham : (n : ), n m |f n| a) (hnm : (n : ), n m f n.succ f n) :
theorem is_cau_of_mono_bounded {α : Type u_1} [linear_ordered_field α] [archimedean α] (f : α) {a : α} {m : } (ham : (n : ), n m |f n| a) (hnm : (n : ), n m f 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 m abv (f m) g m) is_cau_seq has_abs.abs (λ (n : ), (finset.range n).sum (λ (i : ), g i)) is_cau_seq abv (λ (n : ), (finset.range n).sum (λ (i : ), 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 has_abs.abs (λ (m : ), (finset.range m).sum (λ (n : ), abv (f n))) is_cau_seq abv (λ (m : ), (finset.range m).sum (λ (n : ), f n))
theorem is_cau_geo_series {α : Type u_1} [linear_ordered_field α] [archimedean α] {β : Type u_2} [ring β] [nontrivial β] {abv : β α} [is_absolute_value abv] (x : β) (hx1 : abv x < 1) :
is_cau_seq abv (λ (n : ), (finset.range n).sum (λ (m : ), x ^ m))
theorem is_cau_geo_series_const {α : Type u_1} [linear_ordered_field α] [archimedean α] (a : α) {x : α} (hx1 : |x| < 1) :
is_cau_seq has_abs.abs (λ (m : ), (finset.range m).sum (λ (n : ), a * x ^ n))
theorem series_ratio_test {α : Type u_1} [linear_ordered_field α] [archimedean α] {β : Type u_2} [ring β] {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 : ), (finset.range m).sum (λ (n : ), f n))
theorem sum_range_diag_flip {α : Type u_1} [add_comm_monoid α] (n : ) (f : α) :
(finset.range n).sum (λ (m : ), (finset.range (m + 1)).sum (λ (k : ), f k (m - k))) = (finset.range n).sum (λ (m : ), (finset.range (n - m)).sum (λ (k : ), f m k))
theorem abv_sum_le_sum_abv {α : Type u_1} {β : Type u_2} [linear_ordered_field α] {abv : β α} [semiring β] [is_absolute_value abv] {γ : Type u_3} (f : γ β) (s : finset γ) :
abv (s.sum (λ (k : γ), f k)) s.sum (λ (k : γ), abv (f k))
theorem cauchy_product {α : Type u_1} {β : Type u_2} [linear_ordered_field α] {abv : β α} [ring β] [is_absolute_value abv] {a b : β} (ha : is_cau_seq has_abs.abs (λ (m : ), (finset.range m).sum (λ (n : ), abv (a n)))) (hb : is_cau_seq abv (λ (m : ), (finset.range m).sum (λ (n : ), b n))) (ε : α) (ε0 : 0 < ε) :
(i : ), (j : ), j i abv ((finset.range j).sum (λ (k : ), a k) * (finset.range j).sum (λ (k : ), b k) - (finset.range j).sum (λ (n : ), (finset.range (n + 1)).sum (λ (m : ), a m * b (n - m)))) < ε
theorem complex.is_cau_abs_exp (z : ) :
is_cau_seq has_abs.abs (λ (n : ), (finset.range n).sum (λ (m : ), complex.abs (z ^ m / (m.factorial))))
theorem complex.is_cau_exp (z : ) :
is_cau_seq complex.abs (λ (n : ), (finset.range n).sum (λ (m : ), z ^ m / (m.factorial)))
noncomputable def complex.exp' (z : ) :

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

Equations
@[irreducible]
noncomputable def complex.exp (z : ) :

The complex exponential function, defined via its Taylor series

Equations
noncomputable def complex.sin (z : ) :

The complex sine function, defined via exp

Equations
noncomputable def complex.cos (z : ) :

The complex cosine function, defined via exp

Equations
noncomputable def complex.tan (z : ) :

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

Equations
noncomputable def complex.sinh (z : ) :

The complex hyperbolic sine function, defined via exp

Equations
noncomputable def complex.cosh (z : ) :

The complex hyperbolic cosine function, defined via exp

Equations
noncomputable def complex.tanh (z : ) :

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

Equations
noncomputable def real.exp (x : ) :

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

Equations
noncomputable def real.sin (x : ) :

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

Equations
noncomputable def real.cos (x : ) :

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

Equations
noncomputable def real.tan (x : ) :

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

Equations
noncomputable def real.sinh (x : ) :

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

Equations
noncomputable def real.cosh (x : ) :

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

Equations
noncomputable 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_sum {α : Type u_1} (s : finset α) (f : α ) :
complex.exp (s.sum (λ (x : α), f x)) = s.prod (λ (x : α), complex.exp (f x))
theorem complex.exp_nat_mul (x : ) (n : ) :
theorem complex.exp_int_mul (z : ) (n : ) :
@[simp, norm_cast]
@[simp]
theorem complex.exp_of_real_im (x : ) :
@[simp]
theorem complex.sinh_zero  :
@[simp]
@[simp]
theorem complex.cosh_zero  :
@[simp]
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp]
@[simp]
theorem complex.tanh_zero  :
@[simp]
@[simp, norm_cast]
@[simp]
@[simp]
theorem complex.cosh_sq (x : ) :
theorem complex.sinh_sq (x : ) :
@[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, norm_cast]
@[simp]
theorem complex.sin_of_real_im (x : ) :
@[simp, norm_cast]
@[simp]
theorem complex.cos_of_real_im (x : ) :
@[simp]
theorem complex.tan_zero  :
@[simp]
theorem complex.tan_neg (x : ) :
@[simp, norm_cast]
@[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_sq (x : ) :
complex.cos x ^ 2 = 1 / 2 + complex.cos (2 * x) / 2
theorem complex.cos_sq' (x : ) :
theorem complex.sin_sq (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 (s.sum (λ (x : α), f x)) = s.prod (λ (x : α), real.exp (f x))
theorem real.exp_nat_mul (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 : ) :
@[simp]
theorem real.cos_abs (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.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 : ) :
theorem real.cos_sq (x : ) :
real.cos x ^ 2 = 1 / 2 + real.cos (2 * x) / 2
theorem real.cos_sq' (x : ) :
real.cos x ^ 2 = 1 - real.sin x ^ 2
theorem real.sin_sq (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.cosh_eq (x : ) :

The definition of cosh in terms of exp.

@[simp]
theorem real.cosh_zero  :
@[simp]
theorem real.cosh_neg (x : ) :
@[simp]
theorem real.cosh_abs (x : ) :
@[simp]
theorem real.tanh_zero  :
@[simp]
theorem real.tanh_neg (x : ) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem real.cosh_sq_sub_sinh_sq (x : ) :
real.cosh x ^ 2 - real.sinh x ^ 2 = 1
theorem real.cosh_sq (x : ) :
real.cosh x ^ 2 = real.sinh x ^ 2 + 1
theorem real.cosh_sq' (x : ) :
real.cosh x ^ 2 = 1 + real.sinh x ^ 2
theorem real.sinh_sq (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.sum_le_exp_of_nonneg {x : } (hx : 0 x) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i / (i.factorial)) real.exp x
theorem real.quadratic_le_exp_of_nonneg {x : } (hx : 0 x) :
1 + x + x ^ 2 / 2 real.exp x
theorem real.add_one_lt_exp_of_pos {x : } (hx : 0 < x) :
x + 1 < real.exp x
theorem real.add_one_le_exp_of_nonneg {x : } (hx : 0 x) :
x + 1 real.exp x

This is an intermediate result that is later replaced by real.add_one_le_exp; use that lemma instead.

theorem real.one_le_exp {x : } (hx : 0 x) :
theorem real.exp_pos (x : ) :
@[simp]
theorem real.abs_exp (x : ) :
@[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) :
(finset.filter (λ (k : ), n k) (finset.range j)).sum (λ (m : ), 1 / (m.factorial)) (n.succ) / ((n.factorial) * n)
theorem complex.exp_bound {x : } (hx : complex.abs x 1) {n : } (hn : 0 < n) :
theorem complex.exp_bound' {x : } {n : } (hx : complex.abs x / (n.succ) 1 / 2) :
theorem real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
|real.exp x - (finset.range n).sum (λ (m : ), x ^ m / (m.factorial))| |x| ^ n * ((n.succ) / ((n.factorial) * n))
theorem real.exp_bound' {x : } (h1 : 0 x) (h2 : x 1) {n : } (hn : 0 < n) :
real.exp x (finset.range n).sum (λ (m : ), x ^ m / (m.factorial)) + x ^ n * (n + 1) / ((n.factorial) * n)
theorem real.abs_exp_sub_one_le {x : } (hx : |x| 1) :
theorem real.abs_exp_sub_one_sub_id_le {x : } (hx : |x| 1) :
|real.exp x - 1 - x| x ^ 2
noncomputable 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.factorial) * (r₁ - r₂)
theorem real.exp_approx_end (n m : ) (x : ) (e₁ : n + 1 = m) (h : |x| 1) :
|real.exp x - real.exp_near m x 0| |x| ^ m / (m.factorial) * ((m + 1) / m)
theorem real.exp_approx_succ {n : } {x a₁ b₁ : } (m : ) (e₁ : n + 1 = m) (a₂ b₂ : ) (e : |1 + x / m * a₂ - a₁| b₁ - |x| / m * b₂) (h : |real.exp x - real.exp_near m x a₂| |x| ^ m / (m.factorial) * b₂) :
|real.exp x - real.exp_near n x a₁| |x| ^ n / (n.factorial) * b₁
theorem real.exp_approx_end' {n : } {x a b : } (m : ) (e₁ : n + 1 = m) (rm : ) (er : m = rm) (h : |x| 1) (e : |1 - a| b - |x| / rm * ((rm + 1) / rm)) :
theorem real.exp_1_approx_succ_eq {n : } {a₁ b₁ : } {m : } (en : n + 1 = m) {rm : } (er : m = rm) (h : |real.exp 1 - real.exp_near m 1 ((a₁ - 1) * rm)| |1| ^ m / (m.factorial) * (b₁ * rm)) :
|real.exp 1 - real.exp_near n 1 a₁| |1| ^ n / (n.factorial) * b₁
theorem real.exp_approx_start (x a b : ) (h : |real.exp x - real.exp_near 0 x a| |x| ^ 0 / (0.factorial) * b) :
theorem real.cos_bound {x : } (hx : |x| 1) :
|real.cos x - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
theorem real.sin_bound {x : } (hx : |x| 1) :
|real.sin x - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
theorem real.cos_pos_of_le_one {x : } (hx : |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  :
theorem real.exp_bound_div_one_sub_of_interval' {x : } (h1 : 0 < x) (h2 : x < 1) :
real.exp x < 1 / (1 - x)
theorem real.exp_bound_div_one_sub_of_interval {x : } (h1 : 0 x) (h2 : x < 1) :
real.exp x 1 / (1 - x)
theorem real.one_sub_lt_exp_minus_of_pos {y : } (h : 0 < y) :
1 - y < real.exp (-y)
theorem real.one_sub_le_exp_minus_of_nonneg {y : } (h : 0 y) :
1 - y real.exp (-y)
theorem real.add_one_lt_exp_of_neg {x : } (h : x < 0) :
x + 1 < real.exp x
theorem real.add_one_lt_exp_of_nonzero {x : } (hx : x 0) :
x + 1 < real.exp x
theorem real.add_one_le_exp (x : ) :
x + 1 real.exp x
theorem real.one_sub_div_pow_le_exp_neg {n : } {t : } (ht' : t n) :
(1 - t / n) ^ n real.exp (-t)

Extension for the positivity tactic: real.exp is always positive.