data.complex.exponential

source

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) :

is_cau_seq has_abs.abs f

source

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) :

is_cau_seq has_abs.abs f

source

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))

source

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))

source

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))

source

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))

source

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))

source

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))

source

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))

source

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)))) < ε

source

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))))

source

theorem complex.is_cau_exp (z : ℂ) :

is_cau_seq ⇑complex.abs (λ (n : ℕ), (finset.range n).sum (λ (m : ℕ), z ^ m / ↑(m.factorial)))

source

noncomputable 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

complex.exp' z = ⟨λ (n : ℕ), (finset.range n).sum (λ (m : ℕ), z ^ m / ↑(m.factorial)), _⟩

source

@[irreducible]

noncomputable def complex.exp (z : ℂ) :

ℂ

The complex exponential function, defined via its Taylor series

Equations

cexp z = (complex.exp' z).lim

source

noncomputable def complex.sin (z : ℂ) :

ℂ

The complex sine function, defined via exp

Equations

complex.sin z = (cexp (-z * complex.I) - cexp (z * complex.I)) * complex.I / 2

source

noncomputable def complex.cos (z : ℂ) :

ℂ

The complex cosine function, defined via exp

Equations

complex.cos z = (cexp (z * complex.I) + cexp (-z * complex.I)) / 2

source

noncomputable def complex.tan (z : ℂ) :

ℂ

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

Equations

complex.tan z = complex.sin z / complex.cos z

source

noncomputable def complex.sinh (z : ℂ) :

ℂ

The complex hyperbolic sine function, defined via exp

Equations

complex.sinh z = (cexp z - cexp (-z)) / 2

source

noncomputable def complex.cosh (z : ℂ) :

ℂ

The complex hyperbolic cosine function, defined via exp

Equations

complex.cosh z = (cexp z + cexp (-z)) / 2

source

noncomputable def complex.tanh (z : ℂ) :

ℂ

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

Equations

complex.tanh z = complex.sinh z / complex.cosh z

source

noncomputable def real.exp (x : ℝ) :

ℝ

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

Equations

rexp x = (cexp ↑x).re

source

noncomputable def real.sin (x : ℝ) :

ℝ

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

Equations

real.sin x = (complex.sin ↑x).re

source

noncomputable def real.cos (x : ℝ) :

ℝ

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

Equations

real.cos x = (complex.cos ↑x).re

source

noncomputable def real.tan (x : ℝ) :

ℝ

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

Equations

real.tan x = (complex.tan ↑x).re

source

noncomputable def real.sinh (x : ℝ) :

ℝ

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

Equations

real.sinh x = (complex.sinh ↑x).re

source

noncomputable def real.cosh (x : ℝ) :

ℝ

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

Equations

real.cosh x = (complex.cosh ↑x).re

source

noncomputable def real.tanh (x : ℝ) :

ℝ

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

Equations

real.tanh x = (complex.tanh ↑x).re

source

@[simp]

theorem complex.exp_zero :

cexp 0 = 1

source

theorem complex.exp_add (x y : ℂ) :

cexp (x + y) = cexp x * cexp y

source

theorem complex.exp_list_sum (l : list ℂ) :

cexp l.sum = (list.map cexp l).prod

source

theorem complex.exp_multiset_sum (s : multiset ℂ) :

cexp s.sum = (multiset.map cexp s).prod

source

theorem complex.exp_sum {α : Type u_1} (s : finset α) (f : α → ℂ) :

cexp (s.sum (λ (x : α), f x)) = s.prod (λ (x : α), cexp (f x))

source

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

cexp (↑n * x) = cexp x ^ n

source

theorem complex.exp_ne_zero (x : ℂ) :

cexp x ≠ 0

source

theorem complex.exp_neg (x : ℂ) :

cexp (-x) = (cexp x)⁻¹

source

theorem complex.exp_sub (x y : ℂ) :

cexp (x - y) = cexp x / cexp y

source

theorem complex.exp_int_mul (z : ℂ) (n : ℤ) :

cexp (↑n * z) = cexp z ^ n

source

@[simp]

theorem complex.exp_conj (x : ℂ) :

cexp (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (cexp x)

source

@[simp]

theorem complex.of_real_exp_of_real_re (x : ℝ) :

↑((cexp ↑x).re) = cexp ↑x

source

@[simp, norm_cast]

theorem complex.of_real_exp (x : ℝ) :

↑(rexp x) = cexp ↑x

source

@[simp]

theorem complex.exp_of_real_im (x : ℝ) :

(cexp ↑x).im = 0

source

theorem complex.exp_of_real_re (x : ℝ) :

(cexp ↑x).re = rexp x

source

theorem complex.two_sinh (x : ℂ) :

2 * complex.sinh x = cexp x - cexp (-x)

source

theorem complex.two_cosh (x : ℂ) :

2 * complex.cosh x = cexp x + cexp (-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 (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.sinh x)

source

@[simp]

theorem complex.of_real_sinh_of_real_re (x : ℝ) :

↑((complex.sinh ↑x).re) = complex.sinh ↑x

source

@[simp, norm_cast]

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 (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.cosh x)

source

theorem complex.of_real_cosh_of_real_re (x : ℝ) :

↑((complex.cosh ↑x).re) = complex.cosh ↑x

source

@[simp, norm_cast]

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

@[simp]

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 (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.tanh x)

source

@[simp]

theorem complex.of_real_tanh_of_real_re (x : ℝ) :

↑((complex.tanh ↑x).re) = complex.tanh ↑x

source

@[simp, norm_cast]

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

@[simp]

theorem complex.cosh_add_sinh (x : ℂ) :

complex.cosh x + complex.sinh x = cexp x

source

@[simp]

theorem complex.sinh_add_cosh (x : ℂ) :

complex.sinh x + complex.cosh x = cexp x

source

@[simp]

theorem complex.exp_sub_cosh (x : ℂ) :

cexp x - complex.cosh x = complex.sinh x

source

@[simp]

theorem complex.exp_sub_sinh (x : ℂ) :

cexp x - complex.sinh x = complex.cosh x

source

@[simp]

theorem complex.cosh_sub_sinh (x : ℂ) :

complex.cosh x - complex.sinh x = cexp (-x)

source

@[simp]

theorem complex.sinh_sub_cosh (x : ℂ) :

complex.sinh x - complex.cosh x = -cexp (-x)

source

@[simp]

theorem complex.cosh_sq_sub_sinh_sq (x : ℂ) :

complex.cosh x ^ 2 - complex.sinh x ^ 2 = 1

source

theorem complex.cosh_sq (x : ℂ) :

complex.cosh x ^ 2 = complex.sinh x ^ 2 + 1

source

theorem complex.sinh_sq (x : ℂ) :

complex.sinh x ^ 2 = complex.cosh x ^ 2 - 1

source

theorem complex.cosh_two_mul (x : ℂ) :

complex.cosh (2 * x) = complex.cosh x ^ 2 + complex.sinh x ^ 2

source

theorem complex.sinh_two_mul (x : ℂ) :

complex.sinh (2 * x) = 2 * complex.sinh x * complex.cosh x

source

theorem complex.cosh_three_mul (x : ℂ) :

complex.cosh (3 * x) = 4 * complex.cosh x ^ 3 - 3 * complex.cosh x

source

theorem complex.sinh_three_mul (x : ℂ) :

complex.sinh (3 * x) = 4 * complex.sinh x ^ 3 + 3 * complex.sinh x

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 = (cexp (-x * complex.I) - cexp (x * complex.I)) * complex.I

source

theorem complex.two_cos (x : ℂ) :

2 * complex.cos x = cexp (x * complex.I) + cexp (-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.tanh_mul_I (x : ℂ) :

complex.tanh (x * complex.I) = complex.tan x * complex.I

source

theorem complex.cos_mul_I (x : ℂ) :

complex.cos (x * complex.I) = complex.cosh x

source

theorem complex.sin_mul_I (x : ℂ) :

complex.sin (x * complex.I) = complex.sinh x * complex.I

source

theorem complex.tan_mul_I (x : ℂ) :

complex.tan (x * complex.I) = complex.tanh x * complex.I

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_add_mul_I (x y : ℂ) :

complex.sin (x + y * complex.I) = complex.sin x * complex.cosh y + complex.cos x * complex.sinh y * complex.I

source

theorem complex.sin_eq (z : ℂ) :

complex.sin z = complex.sin ↑(z.re) * complex.cosh ↑(z.im) + complex.cos ↑(z.re) * complex.sinh ↑(z.im) * complex.I

source

theorem complex.cos_add_mul_I (x y : ℂ) :

complex.cos (x + y * complex.I) = complex.cos x * complex.cosh y - complex.sin x * complex.sinh y * complex.I

source

theorem complex.cos_eq (z : ℂ) :

complex.cos z = complex.cos ↑(z.re) * complex.cosh ↑(z.im) - complex.sin ↑(z.re) * complex.sinh ↑(z.im) * complex.I

source

theorem complex.sin_sub_sin (x y : ℂ) :

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

source

theorem complex.cos_sub_cos (x y : ℂ) :

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

source

theorem complex.cos_add_cos (x y : ℂ) :

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

source

theorem complex.sin_conj (x : ℂ) :

complex.sin (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.sin x)

source

@[simp]

theorem complex.of_real_sin_of_real_re (x : ℝ) :

↑((complex.sin ↑x).re) = complex.sin ↑x

source

@[simp, norm_cast]

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 (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.cos x)

source

@[simp]

theorem complex.of_real_cos_of_real_re (x : ℝ) :

↑((complex.cos ↑x).re) = complex.cos ↑x

source

@[simp, norm_cast]

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

theorem complex.tan_mul_cos {x : ℂ} (hx : complex.cos x ≠ 0) :

complex.tan x * complex.cos x = complex.sin x

source

@[simp]

theorem complex.tan_neg (x : ℂ) :

complex.tan (-x) = -complex.tan x

source

theorem complex.tan_conj (x : ℂ) :

complex.tan (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.tan x)

source

@[simp]

theorem complex.of_real_tan_of_real_re (x : ℝ) :

↑((complex.tan ↑x).re) = complex.tan ↑x

source

@[simp, norm_cast]

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 = cexp (x * complex.I)

source

theorem complex.cos_sub_sin_I (x : ℂ) :

complex.cos x - complex.sin x * complex.I = cexp (-x * complex.I)

source

@[simp]

theorem complex.sin_sq_add_cos_sq (x : ℂ) :

complex.sin x ^ 2 + complex.cos x ^ 2 = 1

source

@[simp]

theorem complex.cos_sq_add_sin_sq (x : ℂ) :

complex.cos x ^ 2 + complex.sin 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_sq (x : ℂ) :

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

source

theorem complex.cos_sq' (x : ℂ) :

complex.cos x ^ 2 = 1 - complex.sin x ^ 2

source

theorem complex.sin_sq (x : ℂ) :

complex.sin x ^ 2 = 1 - complex.cos x ^ 2

source

theorem complex.inv_one_add_tan_sq {x : ℂ} (hx : complex.cos x ≠ 0) :

(1 + complex.tan x ^ 2)⁻¹ = complex.cos x ^ 2

source

theorem complex.tan_sq_div_one_add_tan_sq {x : ℂ} (hx : complex.cos x ≠ 0) :

complex.tan x ^ 2 / (1 + complex.tan x ^ 2) = complex.sin x ^ 2

source

theorem complex.cos_three_mul (x : ℂ) :

complex.cos (3 * x) = 4 * complex.cos x ^ 3 - 3 * complex.cos x

source

theorem complex.sin_three_mul (x : ℂ) :

complex.sin (3 * x) = 3 * complex.sin x - 4 * complex.sin x ^ 3

source

theorem complex.exp_mul_I (x : ℂ) :

cexp (x * complex.I) = complex.cos x + complex.sin x * complex.I

source

theorem complex.exp_add_mul_I (x y : ℂ) :

cexp (x + y * complex.I) = cexp x * (complex.cos y + complex.sin y * complex.I)

source

theorem complex.exp_eq_exp_re_mul_sin_add_cos (x : ℂ) :

cexp x = cexp ↑(x.re) * (complex.cos ↑(x.im) + complex.sin ↑(x.im) * complex.I)

source

theorem complex.exp_re (x : ℂ) :

(cexp x).re = rexp x.re * real.cos x.im

source

theorem complex.exp_im (x : ℂ) :

(cexp x).im = rexp x.re * real.sin x.im

source

@[simp]

theorem complex.exp_of_real_mul_I_re (x : ℝ) :

(cexp (↑x * complex.I)).re = real.cos x

source

@[simp]

theorem complex.exp_of_real_mul_I_im (x : ℝ) :

(cexp (↑x * complex.I)).im = real.sin x

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 :

rexp 0 = 1

source

theorem real.exp_add (x y : ℝ) :

rexp (x + y) = rexp x * rexp y

source

theorem real.exp_list_sum (l : list ℝ) :

rexp l.sum = (list.map rexp l).prod

source

theorem real.exp_multiset_sum (s : multiset ℝ) :

rexp s.sum = (multiset.map rexp s).prod

source

theorem real.exp_sum {α : Type u_1} (s : finset α) (f : α → ℝ) :

rexp (s.sum (λ (x : α), f x)) = s.prod (λ (x : α), rexp (f x))

source

theorem real.exp_nat_mul (x : ℝ) (n : ℕ) :

rexp (↑n * x) = rexp x ^ n

source

theorem real.exp_ne_zero (x : ℝ) :

rexp x ≠ 0

source

theorem real.exp_neg (x : ℝ) :

rexp (-x) = (rexp x)⁻¹

source

theorem real.exp_sub (x y : ℝ) :

rexp (x - y) = rexp x / rexp 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

@[simp]

theorem real.cos_abs (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.sin_sub_sin (x y : ℝ) :

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

source

theorem real.cos_sub_cos (x y : ℝ) :

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

source

theorem real.cos_add_cos (x y : ℝ) :

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

source

theorem real.tan_eq_sin_div_cos (x : ℝ) :

real.tan x = real.sin x / real.cos x

source

theorem real.tan_mul_cos {x : ℝ} (hx : real.cos x ≠ 0) :

real.tan x * real.cos x = real.sin 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

@[simp]

theorem real.sin_sq_add_cos_sq (x : ℝ) :

real.sin x ^ 2 + real.cos x ^ 2 = 1

source

@[simp]

theorem real.cos_sq_add_sin_sq (x : ℝ) :

real.cos x ^ 2 + real.sin 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 : ℝ) :

|real.sin x| ≤ 1

source

theorem real.abs_cos_le_one (x : ℝ) :

|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.cos_two_mul' (x : ℝ) :

real.cos (2 * x) = real.cos x ^ 2 - real.sin x ^ 2

source

theorem real.sin_two_mul (x : ℝ) :

real.sin (2 * x) = 2 * real.sin x * real.cos x

source

theorem real.cos_sq (x : ℝ) :

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

source

theorem real.cos_sq' (x : ℝ) :

real.cos x ^ 2 = 1 - real.sin x ^ 2

source

theorem real.sin_sq (x : ℝ) :

real.sin x ^ 2 = 1 - real.cos x ^ 2

source

theorem real.abs_sin_eq_sqrt_one_sub_cos_sq (x : ℝ) :

|real.sin x| = √ (1 - real.cos x ^ 2)

source

theorem real.abs_cos_eq_sqrt_one_sub_sin_sq (x : ℝ) :

|real.cos x| = √ (1 - real.sin x ^ 2)

source

theorem real.inv_one_add_tan_sq {x : ℝ} (hx : real.cos x ≠ 0) :

(1 + real.tan x ^ 2)⁻¹ = real.cos x ^ 2

source

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

source

theorem real.inv_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < real.cos x) :

(√ (1 + real.tan x ^ 2))⁻¹ = real.cos x

source

theorem real.tan_div_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < real.cos x) :

real.tan x / √ (1 + real.tan x ^ 2) = real.sin x

source

theorem real.cos_three_mul (x : ℝ) :

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

source

theorem real.sin_three_mul (x : ℝ) :

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

source

theorem real.sinh_eq (x : ℝ) :

real.sinh x = (rexp x - rexp (-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 = (rexp x + rexp (-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

@[simp]

theorem real.cosh_abs (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.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

@[simp]

theorem real.cosh_add_sinh (x : ℝ) :

real.cosh x + real.sinh x = rexp x

source

@[simp]

theorem real.sinh_add_cosh (x : ℝ) :

real.sinh x + real.cosh x = rexp x

source

@[simp]

theorem real.exp_sub_cosh (x : ℝ) :

rexp x - real.cosh x = real.sinh x

source

@[simp]

theorem real.exp_sub_sinh (x : ℝ) :

rexp x - real.sinh x = real.cosh x

source

@[simp]

theorem real.cosh_sub_sinh (x : ℝ) :

real.cosh x - real.sinh x = rexp (-x)

source

@[simp]

theorem real.sinh_sub_cosh (x : ℝ) :

real.sinh x - real.cosh x = -rexp (-x)

source

@[simp]

theorem real.cosh_sq_sub_sinh_sq (x : ℝ) :

real.cosh x ^ 2 - real.sinh x ^ 2 = 1

source

theorem real.cosh_sq (x : ℝ) :

real.cosh x ^ 2 = real.sinh x ^ 2 + 1

source

theorem real.cosh_sq' (x : ℝ) :

real.cosh x ^ 2 = 1 + real.sinh x ^ 2

source

theorem real.sinh_sq (x : ℝ) :

real.sinh x ^ 2 = real.cosh x ^ 2 - 1

source

theorem real.cosh_two_mul (x : ℝ) :

real.cosh (2 * x) = real.cosh x ^ 2 + real.sinh x ^ 2

source

theorem real.sinh_two_mul (x : ℝ) :

real.sinh (2 * x) = 2 * real.sinh x * real.cosh x

source

theorem real.cosh_three_mul (x : ℝ) :

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

source

theorem real.sinh_three_mul (x : ℝ) :

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

source

theorem real.sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) :

(finset.range n).sum (λ (i : ℕ), x ^ i / ↑(i.factorial)) ≤ rexp x

source

theorem real.quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

1 + x + x ^ 2 / 2 ≤ rexp x

source

theorem real.add_one_lt_exp_of_pos {x : ℝ} (hx : 0 < x) :

x + 1 < rexp x

source

theorem real.add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

x + 1 ≤ rexp x

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

source

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

1 ≤ rexp x

source

theorem real.exp_pos (x : ℝ) :

0 < rexp x

source

@[simp]

theorem real.abs_exp (x : ℝ) :

|rexp x| = rexp x

source

theorem real.exp_strict_mono :

strict_mono rexp

source

theorem real.exp_monotone :

monotone rexp

source

@[simp]

theorem real.exp_lt_exp {x y : ℝ} :

rexp x < rexp y ↔ x < y

source

@[simp]

theorem real.exp_le_exp {x y : ℝ} :

rexp x ≤ rexp y ↔ x ≤ y

source

theorem real.exp_injective :

function.injective rexp

source

@[simp]

theorem real.exp_eq_exp {x y : ℝ} :

rexp x = rexp y ↔ x = y

source

@[simp]

theorem real.exp_eq_one_iff (x : ℝ) :

rexp x = 1 ↔ x = 0

source

@[simp]

theorem real.one_lt_exp_iff {x : ℝ} :

1 < rexp x ↔ 0 < x

source

@[simp]

theorem real.exp_lt_one_iff {x : ℝ} :

rexp x < 1 ↔ x < 0

source

@[simp]

theorem real.exp_le_one_iff {x : ℝ} :

rexp x ≤ 1 ↔ x ≤ 0

source

@[simp]

theorem real.one_le_exp_iff {x : ℝ} :

1 ≤ rexp x ↔ 0 ≤ x

source

theorem real.cosh_pos (x : ℝ) :

0 < real.cosh x

real.cosh is always positive

source

theorem real.sinh_lt_cosh (x : ℝ) :

real.sinh x < real.cosh x

source

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)

source

theorem complex.exp_bound {x : ℂ} (hx : ⇑complex.abs x ≤ 1) {n : ℕ} (hn : 0 < n) :

⇑complex.abs (cexp x - (finset.range n).sum (λ (m : ℕ), x ^ m / ↑(m.factorial))) ≤ ⇑complex.abs x ^ n * (↑(n.succ) * (↑(n.factorial) * ↑n)⁻¹)

source

theorem complex.exp_bound' {x : ℂ} {n : ℕ} (hx : ⇑complex.abs x / ↑(n.succ) ≤ 1 / 2) :

⇑complex.abs (cexp x - (finset.range n).sum (λ (m : ℕ), x ^ m / ↑(m.factorial))) ≤ ⇑complex.abs x ^ n / ↑(n.factorial) * 2

source

theorem complex.abs_exp_sub_one_le {x : ℂ} (hx : ⇑complex.abs x ≤ 1) :

⇑complex.abs (cexp x - 1) ≤ 2 * ⇑complex.abs x

source

theorem complex.abs_exp_sub_one_sub_id_le {x : ℂ} (hx : ⇑complex.abs x ≤ 1) :

⇑complex.abs (cexp x - 1 - x) ≤ ⇑complex.abs x ^ 2

source

theorem real.exp_bound {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) :

|rexp x - (finset.range n).sum (λ (m : ℕ), x ^ m / ↑(m.factorial))| ≤ |x| ^ n * (↑(n.succ) / (↑(n.factorial) * ↑n))

source

theorem real.exp_bound' {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) {n : ℕ} (hn : 0 < n) :

rexp x ≤ (finset.range n).sum (λ (m : ℕ), x ^ m / ↑(m.factorial)) + x ^ n * (↑n + 1) / (↑(n.factorial) * ↑n)

source

theorem real.abs_exp_sub_one_le {x : ℝ} (hx : |x| ≤ 1) :

|rexp x - 1| ≤ 2 * |x|

source

theorem real.abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) :

|rexp x - 1 - x| ≤ x ^ 2

source

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

real.exp_near n x r = (finset.range n).sum (λ (m : ℕ), x ^ m / ↑(m.factorial)) + x ^ n / ↑(n.factorial) * r

source

@[simp]

theorem real.exp_near_zero (x r : ℝ) :

real.exp_near 0 x r = r

source

@[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)

source

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₂)

source

theorem real.exp_approx_end (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) :

|rexp x - real.exp_near m x 0| ≤ |x| ^ m / ↑(m.factorial) * ((↑m + 1) / ↑m)

source

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 : |rexp x - real.exp_near m x a₂| ≤ |x| ^ m / ↑(m.factorial) * b₂) :

|rexp x - real.exp_near n x a₁| ≤ |x| ^ n / ↑(n.factorial) * b₁

source

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)) :

|rexp x - real.exp_near n x a| ≤ |x| ^ n / ↑(n.factorial) * b

source

theorem real.exp_1_approx_succ_eq {n : ℕ} {a₁ b₁ : ℝ} {m : ℕ} (en : n + 1 = m) {rm : ℝ} (er : ↑m = rm) (h : |rexp 1 - real.exp_near m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑(m.factorial) * (b₁ * rm)) :