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.
theorem
is_cau_of_decreasing_bounded
{α : Type u_1}
[discrete_linear_ordered_field α]
[archimedean α]
(f : ℕ → α)
{a : α}
{m : ℕ} :
theorem
is_cau_of_mono_bounded
{α : Type u_1}
[discrete_linear_ordered_field α]
[archimedean α]
(f : ℕ → α)
{a : α}
{m : ℕ} :
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 ≤ m → abv (f m) ≤ g m) → is_cau_seq 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 β]
[discrete_linear_ordered_field α]
{abv : β → α}
[is_absolute_value abv]
{f : ℕ → β} :
is_cau_seq 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}
[discrete_linear_ordered_field α]
[archimedean α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
abv x < 1 → is_cau_seq abv (λ (n : ℕ), (finset.range n).sum (λ (m : ℕ), x ^ m))
theorem
is_cau_geo_series_const
{α : Type u_1}
[discrete_linear_ordered_field α]
[archimedean α]
(a : α)
{x : α} :
abs x < 1 → is_cau_seq abs (λ (m : ℕ), (finset.range m).sum (λ (n : ℕ), 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 : α) :
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
sum_range_sub_sum_range
{α : Type u_1}
[add_comm_group α]
{f : ℕ → α}
{n m : ℕ} :
n ≤ m → (finset.range m).sum (λ (k : ℕ), f k) - (finset.range n).sum (λ (k : ℕ), f k) = (finset.filter (λ (k : ℕ), n ≤ k) (finset.range m)).sum (λ (k : ℕ), 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 γ) :
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 : ℕ), (finset.range m).sum (λ (n : ℕ), abv (a n))))
(hb : is_cau_seq abv (λ (m : ℕ), (finset.range m).sum (λ (n : ℕ), b n)))
(ε : α) :
theorem
complex.is_cau_abs_exp
(z : ℂ) :
is_cau_seq abs (λ (n : ℕ), (finset.range n).sum (λ (m : ℕ), complex.abs (z ^ m / ↑(m.fact))))
theorem
complex.is_cau_exp
(z : ℂ) :
is_cau_seq complex.abs (λ (n : ℕ), (finset.range n).sum (λ (m : ℕ), z ^ m / ↑(m.fact)))
The Cauchy sequence consisting of partial sums of the Taylor series of the complex exponential function
The complex exponential function, defined via its Taylor series
Equations
- complex.exp z = (complex.exp' z).lim
The complex sine function, defined via exp
Equations
- complex.sin z = (complex.exp (-z * complex.I) - complex.exp (z * complex.I)) * complex.I / 2
The complex cosine function, defined via exp
Equations
- complex.cos z = (complex.exp (z * complex.I) + complex.exp (-z * complex.I)) / 2
The complex tangent function, defined as sin z / cos z
Equations
- complex.tan z = complex.sin z / complex.cos z
The complex hyperbolic sine function, defined via exp
Equations
- complex.sinh z = (complex.exp z - complex.exp (-z)) / 2
The complex hyperbolic cosine function, defined via exp
Equations
- complex.cosh z = (complex.exp z + complex.exp (-z)) / 2
The complex hyperbolic tangent function, defined as sinh z / cosh z
Equations
- complex.tanh z = complex.sinh z / complex.cosh z
The real hypebolic sine function, defined as the real part of the complex hyperbolic sine
Equations
- real.sinh x = (complex.sinh ↑x).re
The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine
Equations
- real.cosh x = (complex.cosh ↑x).re
The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent
Equations
- real.tanh x = (complex.tanh ↑x).re
theorem
complex.exp_multiset_sum
(s : multiset ℂ) :
complex.exp s.sum = (multiset.map complex.exp s).prod
theorem
complex.exp_sum
{α : Type u_1}
(s : finset α)
(f : α → ℂ) :
complex.exp (s.sum (λ (x : α), f x)) = s.prod (λ (x : α), complex.exp (f x))
@[simp]
@[simp]
theorem
complex.sinh_add
(x y : ℂ) :
complex.sinh (x + y) = complex.sinh x * complex.cosh y + complex.cosh x * complex.sinh y
theorem
complex.cosh_add
(x y : ℂ) :
complex.cosh (x + y) = complex.cosh x * complex.cosh y + complex.sinh x * complex.sinh y
theorem
complex.sinh_sub
(x y : ℂ) :
complex.sinh (x - y) = complex.sinh x * complex.cosh y - complex.cosh x * complex.sinh y
theorem
complex.cosh_sub
(x y : ℂ) :
complex.cosh (x - y) = complex.cosh x * complex.cosh y - complex.sinh x * complex.sinh y
@[simp]
@[simp]
@[simp]
theorem
complex.two_sin
(x : ℂ) :
2 * complex.sin x = (complex.exp (-x * complex.I) - complex.exp (x * complex.I)) * complex.I
theorem
complex.two_cos
(x : ℂ) :
2 * complex.cos x = complex.exp (x * complex.I) + complex.exp (-x * complex.I)
theorem
complex.sin_add
(x y : ℂ) :
complex.sin (x + y) = complex.sin x * complex.cos y + complex.cos x * complex.sin y
theorem
complex.cos_add
(x y : ℂ) :
complex.cos (x + y) = complex.cos x * complex.cos y - complex.sin x * complex.sin y
theorem
complex.sin_sub
(x y : ℂ) :
complex.sin (x - y) = complex.sin x * complex.cos y - complex.cos x * complex.sin y
theorem
complex.cos_sub
(x y : ℂ) :
complex.cos (x - y) = complex.cos x * complex.cos y + complex.sin x * complex.sin y
@[simp]
@[simp]
@[simp]
theorem
complex.cos_add_sin_I
(x : ℂ) :
complex.cos x + complex.sin x * complex.I = complex.exp (x * complex.I)
theorem
complex.cos_sub_sin_I
(x : ℂ) :
complex.cos x - complex.sin x * complex.I = complex.exp (-x * complex.I)
theorem
complex.exp_mul_I
(x : ℂ) :
complex.exp (x * complex.I) = complex.cos x + complex.sin x * complex.I
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)
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)
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
theorem
complex.abs_exp_sub_one_le
{x : ℂ} :
complex.abs x ≤ 1 → complex.abs (complex.exp x - 1) ≤ 2 * complex.abs x
theorem
complex.abs_exp_sub_one_sub_id_le
{x : ℂ} :
complex.abs x ≤ 1 → complex.abs (complex.exp x - 1 - x) ≤ complex.abs x ^ 2
theorem
complex.abs_cos_add_sin_mul_I
(x : ℝ) :
complex.abs (complex.cos ↑x + complex.sin ↑x * complex.I) = 1
theorem
complex.abs_exp_eq_iff_re_eq
{x y : ℂ} :
complex.abs (complex.exp x) = complex.abs (complex.exp y) ↔ x.re = y.re