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 isCauSeq_of_decreasing_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ (n : ℕ), n ≥ m → |f n| ≤ a) (hnm : ∀ (n : ℕ), n ≥ m → f (Nat.succ n) ≤ f n) : IsCauSeq abs f

theorem isCauSeq_of_mono_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ (n : ℕ), n ≥ m → |f n| ≤ a) (hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)) : IsCauSeq abs f

theorem isCauSeq_series_of_abv_le_of_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] [LinearOrderedField α] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β} {g : ℕ → α} (n : ℕ) : (∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m) → (IsCauSeq abs fun n => Finset.sum (Finset.range n) fun i => g i) → IsCauSeq abv fun n => Finset.sum (Finset.range n) fun i => f i

theorem isCauSeq_series_of_abv_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] [LinearOrderedField α] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β} : (IsCauSeq abs fun m => Finset.sum (Finset.range m) fun n => abv (f n)) → IsCauSeq abv fun m => Finset.sum (Finset.range m) fun n => f n

theorem isCauSeq_geo_series {α : Type u_1} [LinearOrderedField α] [Archimedean α] {β : Type u_2} [Ring β] [Nontrivial β] {abv : β → α} [IsAbsoluteValue abv] (x : β) (hx1 : abv x < 1) : IsCauSeq abv fun n => Finset.sum (Finset.range n) fun m => x ^ m

theorem isCauSeq_geo_series_const {α : Type u_1} [LinearOrderedField α] [Archimedean α] (a : α) {x : α} (hx1 : |x| < 1) : IsCauSeq abs fun m => Finset.sum (Finset.range m) fun n => a * x ^ n

theorem series_ratio_test {α : Type u_1} [LinearOrderedField α] [Archimedean α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β} (n : ℕ) (r : α) (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) : IsCauSeq abv fun m => Finset.sum (Finset.range m) fun n => f n

theorem sum_range_diag_flip {α : Type u_3} [AddCommMonoid α] (n : ℕ) (f : ℕ → ℕ → α) : (Finset.sum (Finset.range n) fun m => Finset.sum (Finset.range (m + 1)) fun k => f k (m - k)) = Finset.sum (Finset.range n) fun m => Finset.sum (Finset.range (n - m)) fun k => f m k

theorem abv_sum_le_sum_abv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {abv : β → α} [Semiring β] [IsAbsoluteValue abv] {γ : Type u_3} (f : γ → β) (s : Finset γ) : abv (Finset.sum s fun k => f k) ≤ Finset.sum s fun k => abv (f k)

theorem cauchy_product {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {abv : β → α} [Ring β] [IsAbsoluteValue abv] {a : ℕ → β} {b : ℕ → β} (ha : IsCauSeq abs fun m => Finset.sum (Finset.range m) fun n => abv (a n)) (hb : IsCauSeq abv fun m => Finset.sum (Finset.range m) fun n => b n) (ε : α) (ε0 : 0 < ε) : ∃ i, ∀ (j : ℕ), j ≥ i → abv (((Finset.sum (Finset.range j) fun k => a k) * Finset.sum (Finset.range j) fun k => b k) - Finset.sum (Finset.range j) fun n => Finset.sum (Finset.range (n + 1)) fun m => a m * b (n - m)) < ε

theorem Complex.isCauSeq_abs_exp (z : ℂ) : IsCauSeq abs fun n => Finset.sum (Finset.range n) fun m => ↑Complex.abs (z ^ m / ↑(Nat.factorial m))

theorem Complex.isCauSeq_exp (z : ℂ) : IsCauSeq ↑Complex.abs fun n => Finset.sum (Finset.range n) fun m => z ^ m / ↑(Nat.factorial m)

def Complex.exp' (z : ℂ) : CauSeq ℂ ↑Complex.abs

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

def Complex.exp (z : ℂ) : ℂ

The complex exponential function, defined via its Taylor series

def Complex.sin (z : ℂ) : ℂ

The complex sine function, defined via exp

def Complex.cos (z : ℂ) : ℂ

The complex cosine function, defined via exp

def Complex.tan (z : ℂ) : ℂ

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

def Complex.sinh (z : ℂ) : ℂ

The complex hyperbolic sine function, defined via exp

def Complex.cosh (z : ℂ) : ℂ

The complex hyperbolic cosine function, defined via exp

def Complex.tanh (z : ℂ) : ℂ

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

def Complex.termCexp : Lean.ParserDescr

scoped notation for the complex exponential function

def Real.exp (x : ℝ) : ℝ

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

def Real.sin (x : ℝ) : ℝ

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

def Real.cos (x : ℝ) : ℝ

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

def Real.tan (x : ℝ) : ℝ

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

def Real.sinh (x : ℝ) : ℝ

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

def Real.cosh (x : ℝ) : ℝ

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

def Real.tanh (x : ℝ) : ℝ

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

def Real.termRexp : Lean.ParserDescr

scoped notation for the real exponential function

@[simp]

theorem Complex.exp_zero : Complex.exp 0 = 1

theorem Complex.exp_add (x : ℂ) (y : ℂ) : Complex.exp (x + y) = Complex.exp x * Complex.exp y

noncomputable def Complex.expMonoidHom : Multiplicative ℂ →* ℂ

the exponential function as a monoid hom from Multiplicative ℂ to ℂ

theorem Complex.exp_list_sum (l : List ℂ) : Complex.exp (List.sum l) = List.prod (List.map Complex.exp l)

theorem Complex.exp_multiset_sum (s : Multiset ℂ) : Complex.exp (Multiset.sum s) = Multiset.prod (Multiset.map Complex.exp s)

theorem Complex.exp_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : Complex.exp (Finset.sum s fun x => f x) = Finset.prod s fun x => Complex.exp (f x)

theorem Complex.exp_nat_mul (x : ℂ) (n : ℕ) : Complex.exp (↑n * x) = Complex.exp x ^ n

theorem Complex.exp_ne_zero (x : ℂ) : Complex.exp x ≠ 0

theorem Complex.exp_neg (x : ℂ) : Complex.exp (-x) = (Complex.exp x)⁻¹

theorem Complex.exp_sub (x : ℂ) (y : ℂ) : Complex.exp (x - y) = Complex.exp x / Complex.exp y

theorem Complex.exp_int_mul (z : ℂ) (n : ℤ) : Complex.exp (↑n * z) = Complex.exp z ^ n

@[simp]

theorem Complex.exp_conj (x : ℂ) : Complex.exp (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.exp x)

@[simp]

theorem Complex.ofReal_exp_ofReal_re (x : ℝ) : ↑(Complex.exp ↑x).re = Complex.exp ↑x

@[simp]

theorem Complex.ofReal_exp (x : ℝ) : ↑(Real.exp x) = Complex.exp ↑x

@[simp]

theorem Complex.exp_ofReal_im (x : ℝ) : (Complex.exp ↑x).im = 0

theorem Complex.exp_ofReal_re (x : ℝ) : (Complex.exp ↑x).re = Real.exp x

theorem Complex.two_sinh (x : ℂ) : 2 * Complex.sinh x = Complex.exp x - Complex.exp (-x)

theorem Complex.two_cosh (x : ℂ) : 2 * Complex.cosh x = Complex.exp x + Complex.exp (-x)

@[simp]

theorem Complex.sinh_zero : Complex.sinh 0 = 0

@[simp]

theorem Complex.sinh_neg (x : ℂ) : Complex.sinh (-x) = -Complex.sinh x

theorem Complex.sinh_add (x : ℂ) (y : ℂ) : Complex.sinh (x + y) = Complex.sinh x * Complex.cosh y + Complex.cosh x * Complex.sinh y

@[simp]

theorem Complex.cosh_zero : Complex.cosh 0 = 1

@[simp]

theorem Complex.cosh_neg (x : ℂ) : Complex.cosh (-x) = Complex.cosh x

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

theorem Complex.sinh_conj (x : ℂ) : Complex.sinh (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.sinh x)

@[simp]

theorem Complex.ofReal_sinh_ofReal_re (x : ℝ) : ↑(Complex.sinh ↑x).re = Complex.sinh ↑x

@[simp]

theorem Complex.ofReal_sinh (x : ℝ) : ↑(Real.sinh x) = Complex.sinh ↑x

@[simp]

theorem Complex.sinh_ofReal_im (x : ℝ) : (Complex.sinh ↑x).im = 0

theorem Complex.sinh_ofReal_re (x : ℝ) : (Complex.sinh ↑x).re = Real.sinh x

theorem Complex.cosh_conj (x : ℂ) : Complex.cosh (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.cosh x)

theorem Complex.ofReal_cosh_ofReal_re (x : ℝ) : ↑(Complex.cosh ↑x).re = Complex.cosh ↑x

@[simp]

theorem Complex.ofReal_cosh (x : ℝ) : ↑(Real.cosh x) = Complex.cosh ↑x

@[simp]

theorem Complex.cosh_ofReal_im (x : ℝ) : (Complex.cosh ↑x).im = 0

@[simp]

theorem Complex.cosh_ofReal_re (x : ℝ) : (Complex.cosh ↑x).re = Real.cosh x

theorem Complex.tanh_eq_sinh_div_cosh (x : ℂ) : Complex.tanh x = Complex.sinh x / Complex.cosh x

@[simp]

theorem Complex.tanh_zero : Complex.tanh 0 = 0

@[simp]

theorem Complex.tanh_neg (x : ℂ) : Complex.tanh (-x) = -Complex.tanh x

theorem Complex.tanh_conj (x : ℂ) : Complex.tanh (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.tanh x)

@[simp]

theorem Complex.ofReal_tanh_ofReal_re (x : ℝ) : ↑(Complex.tanh ↑x).re = Complex.tanh ↑x

@[simp]

theorem Complex.ofReal_tanh (x : ℝ) : ↑(Real.tanh x) = Complex.tanh ↑x

@[simp]

theorem Complex.tanh_ofReal_im (x : ℝ) : (Complex.tanh ↑x).im = 0

theorem Complex.tanh_ofReal_re (x : ℝ) : (Complex.tanh ↑x).re = Real.tanh x

@[simp]

theorem Complex.cosh_add_sinh (x : ℂ) : Complex.cosh x + Complex.sinh x = Complex.exp x

@[simp]

theorem Complex.sinh_add_cosh (x : ℂ) : Complex.sinh x + Complex.cosh x = Complex.exp x

@[simp]

theorem Complex.exp_sub_cosh (x : ℂ) : Complex.exp x - Complex.cosh x = Complex.sinh x

@[simp]

theorem Complex.exp_sub_sinh (x : ℂ) : Complex.exp x - Complex.sinh x = Complex.cosh x

@[simp]

theorem Complex.cosh_sub_sinh (x : ℂ) : Complex.cosh x - Complex.sinh x = Complex.exp (-x)

@[simp]

theorem Complex.sinh_sub_cosh (x : ℂ) : Complex.sinh x - Complex.cosh x = -Complex.exp (-x)

@[simp]

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

theorem Complex.cosh_sq (x : ℂ) : Complex.cosh x ^ 2 = Complex.sinh x ^ 2 + 1

theorem Complex.sinh_sq (x : ℂ) : Complex.sinh x ^ 2 = Complex.cosh x ^ 2 - 1

theorem Complex.cosh_two_mul (x : ℂ) : Complex.cosh (2 * x) = Complex.cosh x ^ 2 + Complex.sinh x ^ 2

theorem Complex.sinh_two_mul (x : ℂ) : Complex.sinh (2 * x) = 2 * Complex.sinh x * Complex.cosh x

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

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

@[simp]

theorem Complex.sin_zero : Complex.sin 0 = 0

@[simp]

theorem Complex.sin_neg (x : ℂ) : Complex.sin (-x) = -Complex.sin x

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.sinh_mul_I (x : ℂ) : Complex.sinh (x * Complex.I) = Complex.sin x * Complex.I

theorem Complex.cosh_mul_I (x : ℂ) : Complex.cosh (x * Complex.I) = Complex.cos x

theorem Complex.tanh_mul_I (x : ℂ) : Complex.tanh (x * Complex.I) = Complex.tan x * Complex.I

theorem Complex.cos_mul_I (x : ℂ) : Complex.cos (x * Complex.I) = Complex.cosh x

theorem Complex.sin_mul_I (x : ℂ) : Complex.sin (x * Complex.I) = Complex.sinh x * Complex.I

theorem Complex.tan_mul_I (x : ℂ) : Complex.tan (x * Complex.I) = Complex.tanh 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

@[simp]

theorem Complex.cos_zero : Complex.cos 0 = 1

@[simp]

theorem Complex.cos_neg (x : ℂ) : Complex.cos (-x) = Complex.cos x

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

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

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

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

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

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)

theorem Complex.sin_conj (x : ℂ) : Complex.sin (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.sin x)

@[simp]

theorem Complex.ofReal_sin_ofReal_re (x : ℝ) : ↑(Complex.sin ↑x).re = Complex.sin ↑x

@[simp]

theorem Complex.ofReal_sin (x : ℝ) : ↑(Real.sin x) = Complex.sin ↑x

@[simp]

theorem Complex.sin_ofReal_im (x : ℝ) : (Complex.sin ↑x).im = 0

theorem Complex.sin_ofReal_re (x : ℝ) : (Complex.sin ↑x).re = Real.sin x

theorem Complex.cos_conj (x : ℂ) : Complex.cos (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.cos x)

@[simp]

theorem Complex.ofReal_cos_ofReal_re (x : ℝ) : ↑(Complex.cos ↑x).re = Complex.cos ↑x

@[simp]

theorem Complex.ofReal_cos (x : ℝ) : ↑(Real.cos x) = Complex.cos ↑x

@[simp]

theorem Complex.cos_ofReal_im (x : ℝ) : (Complex.cos ↑x).im = 0

theorem Complex.cos_ofReal_re (x : ℝ) : (Complex.cos ↑x).re = Real.cos x

@[simp]

theorem Complex.tan_zero : Complex.tan 0 = 0

theorem Complex.tan_eq_sin_div_cos (x : ℂ) : Complex.tan x = Complex.sin x / Complex.cos x

theorem Complex.tan_mul_cos {x : ℂ} (hx : Complex.cos x ≠ 0) : Complex.tan x * Complex.cos x = Complex.sin x

@[simp]

theorem Complex.tan_neg (x : ℂ) : Complex.tan (-x) = -Complex.tan x

theorem Complex.tan_conj (x : ℂ) : Complex.tan (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (Complex.tan x)

@[simp]

theorem Complex.ofReal_tan_ofReal_re (x : ℝ) : ↑(Complex.tan ↑x).re = Complex.tan ↑x

@[simp]

theorem Complex.ofReal_tan (x : ℝ) : ↑(Real.tan x) = Complex.tan ↑x

@[simp]

theorem Complex.tan_ofReal_im (x : ℝ) : (Complex.tan ↑x).im = 0

theorem Complex.tan_ofReal_re (x : ℝ) : (Complex.tan ↑x).re = Real.tan x

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)

@[simp]

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

@[simp]

theorem Complex.cos_sq_add_sin_sq (x : ℂ) : Complex.cos x ^ 2 + Complex.sin x ^ 2 = 1

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

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

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

theorem Complex.cos_sq (x : ℂ) : Complex.cos x ^ 2 = 1 / 2 + Complex.cos (2 * x) / 2

theorem Complex.cos_sq' (x : ℂ) : Complex.cos x ^ 2 = 1 - Complex.sin x ^ 2

theorem Complex.sin_sq (x : ℂ) : Complex.sin x ^ 2 = 1 - Complex.cos x ^ 2

theorem Complex.inv_one_add_tan_sq {x : ℂ} (hx : Complex.cos x ≠ 0) : (1 + Complex.tan x ^ 2)⁻¹ = Complex.cos x ^ 2

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

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

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

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.exp_re (x : ℂ) : (Complex.exp x).re = Real.exp x.re * Real.cos x.im

theorem Complex.exp_im (x : ℂ) : (Complex.exp x).im = Real.exp x.re * Real.sin x.im

@[simp]

theorem Complex.exp_ofReal_mul_I_re (x : ℝ) : (Complex.exp (↑x * Complex.I)).re = Real.cos x

@[simp]

theorem Complex.exp_ofReal_mul_I_im (x : ℝ) : (Complex.exp (↑x * Complex.I)).im = Real.sin x

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

@[simp]

theorem Real.exp_zero : Real.exp 0 = 1

theorem Real.exp_add (x : ℝ) (y : ℝ) : Real.exp (x + y) = Real.exp x * Real.exp y

noncomputable def Real.expMonoidHom : Multiplicative ℝ →* ℝ

the exponential function as a monoid hom from Multiplicative ℝ to ℝ

theorem Real.exp_list_sum (l : List ℝ) : Real.exp (List.sum l) = List.prod (List.map Real.exp l)

theorem Real.exp_multiset_sum (s : Multiset ℝ) : Real.exp (Multiset.sum s) = Multiset.prod (Multiset.map Real.exp s)

theorem Real.exp_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) : Real.exp (Finset.sum s fun x => f x) = Finset.prod s fun x => 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 : ℝ) : Real.exp x ≠ 0

theorem Real.exp_neg (x : ℝ) : Real.exp (-x) = (Real.exp x)⁻¹

theorem Real.exp_sub (x : ℝ) (y : ℝ) : Real.exp (x - y) = Real.exp x / Real.exp y

@[simp]

theorem Real.sin_zero : Real.sin 0 = 0

@[simp]

theorem Real.sin_neg (x : ℝ) : Real.sin (-x) = -Real.sin x

theorem Real.sin_add (x : ℝ) (y : ℝ) : Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y

@[simp]

theorem Real.cos_zero : Real.cos 0 = 1

@[simp]

theorem Real.cos_neg (x : ℝ) : Real.cos (-x) = Real.cos x

@[simp]

theorem Real.cos_abs (x : ℝ) : Real.cos |x| = Real.cos x

theorem Real.cos_add (x : ℝ) (y : ℝ) : Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y

theorem Real.sin_sub (x : ℝ) (y : ℝ) : Real.sin (x - y) = Real.sin x * Real.cos y - Real.cos x * Real.sin y

theorem Real.cos_sub (x : ℝ) (y : ℝ) : Real.cos (x - y) = Real.cos x * Real.cos y + Real.sin x * Real.sin 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_eq_sin_div_cos (x : ℝ) : Real.tan x = Real.sin x / Real.cos x

theorem Real.tan_mul_cos {x : ℝ} (hx : Real.cos x ≠ 0) : Real.tan x * Real.cos x = Real.sin x

@[simp]

theorem Real.tan_zero : Real.tan 0 = 0

@[simp]

theorem Real.tan_neg (x : ℝ) : Real.tan (-x) = -Real.tan 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 : ℝ) : |Real.sin x| ≤ 1

theorem Real.abs_cos_le_one (x : ℝ) : |Real.cos x| ≤ 1

theorem Real.sin_le_one (x : ℝ) : Real.sin x ≤ 1

theorem Real.cos_le_one (x : ℝ) : Real.cos x ≤ 1

theorem Real.neg_one_le_sin (x : ℝ) : -1 ≤ Real.sin x

theorem Real.neg_one_le_cos (x : ℝ) : -1 ≤ Real.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_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.abs_sin_eq_sqrt_one_sub_cos_sq (x : ℝ) : |Real.sin x| = Real.sqrt (1 - Real.cos x ^ 2)

theorem Real.abs_cos_eq_sqrt_one_sub_sin_sq (x : ℝ) : |Real.cos x| = Real.sqrt (1 - Real.sin 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.inv_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < Real.cos x) : (Real.sqrt (1 + Real.tan x ^ 2))⁻¹ = Real.cos x

theorem Real.tan_div_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < Real.cos x) : Real.tan x / Real.sqrt (1 + Real.tan x ^ 2) = Real.sin x

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 : ℝ) : Real.sinh x = (Real.exp x - Real.exp (-x)) / 2

The definition of sinh in terms of exp.

@[simp]

theorem Real.sinh_zero : Real.sinh 0 = 0

@[simp]

theorem Real.sinh_neg (x : ℝ) : Real.sinh (-x) = -Real.sinh x

theorem Real.sinh_add (x : ℝ) (y : ℝ) : Real.sinh (x + y) = Real.sinh x * Real.cosh y + Real.cosh x * Real.sinh y

theorem Real.cosh_eq (x : ℝ) : Real.cosh x = (Real.exp x + Real.exp (-x)) / 2

The definition of cosh in terms of exp.

@[simp]

theorem Real.cosh_zero : Real.cosh 0 = 1

@[simp]

theorem Real.cosh_neg (x : ℝ) : Real.cosh (-x) = Real.cosh x

@[simp]

theorem Real.cosh_abs (x : ℝ) : Real.cosh |x| = Real.cosh x

theorem Real.cosh_add (x : ℝ) (y : ℝ) : Real.cosh (x + y) = Real.cosh x * Real.cosh y + Real.sinh x * Real.sinh y

theorem Real.sinh_sub (x : ℝ) (y : ℝ) : Real.sinh (x - y) = Real.sinh x * Real.cosh y - Real.cosh x * Real.sinh y

theorem Real.cosh_sub (x : ℝ) (y : ℝ) : Real.cosh (x - y) = Real.cosh x * Real.cosh y - Real.sinh x * Real.sinh y

theorem Real.tanh_eq_sinh_div_cosh (x : ℝ) : Real.tanh x = Real.sinh x / Real.cosh x

@[simp]

theorem Real.tanh_zero : Real.tanh 0 = 0

@[simp]

theorem Real.tanh_neg (x : ℝ) : Real.tanh (-x) = -Real.tanh x

@[simp]

theorem Real.cosh_add_sinh (x : ℝ) : Real.cosh x + Real.sinh x = Real.exp x

@[simp]

theorem Real.sinh_add_cosh (x : ℝ) : Real.sinh x + Real.cosh x = Real.exp x

@[simp]

theorem Real.exp_sub_cosh (x : ℝ) : Real.exp x - Real.cosh x = Real.sinh x

@[simp]

theorem Real.exp_sub_sinh (x : ℝ) : Real.exp x - Real.sinh x = Real.cosh x

@[simp]

theorem Real.cosh_sub_sinh (x : ℝ) : Real.cosh x - Real.sinh x = Real.exp (-x)

@[simp]

theorem Real.sinh_sub_cosh (x : ℝ) : Real.sinh x - Real.cosh x = -Real.exp (-x)

@[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 : ℝ) : Real.cosh (2 * x) = Real.cosh x ^ 2 + Real.sinh x ^ 2

theorem Real.sinh_two_mul (x : ℝ) : Real.sinh (2 * x) = 2 * Real.sinh x * Real.cosh 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.sum (Finset.range n) fun i => x ^ i / ↑(Nat.factorial i)) ≤ 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) : 1 ≤ Real.exp x

theorem Real.exp_pos (x : ℝ) : 0 < Real.exp x

@[simp]

theorem Real.abs_exp (x : ℝ) : |Real.exp x| = Real.exp x

theorem Real.exp_strictMono : StrictMono Real.exp

theorem Real.exp_lt_exp_of_lt {x : ℝ} {y : ℝ} (h : x < y) : Real.exp x < Real.exp y

theorem Real.exp_monotone : Monotone Real.exp

theorem Real.exp_le_exp_of_le {x : ℝ} {y : ℝ} (h : x ≤ y) : Real.exp x ≤ Real.exp y

@[simp]

theorem Real.exp_lt_exp {x : ℝ} {y : ℝ} : Real.exp x < Real.exp y ↔ x < y

@[simp]

theorem Real.exp_le_exp {x : ℝ} {y : ℝ} : Real.exp x ≤ Real.exp y ↔ x ≤ y

theorem Real.exp_injective : Function.Injective Real.exp

@[simp]

theorem Real.exp_eq_exp {x : ℝ} {y : ℝ} : Real.exp x = Real.exp y ↔ 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 : ℝ} : Real.exp x ≤ 1 ↔ x ≤ 0

@[simp]

theorem Real.one_le_exp_iff {x : ℝ} : 1 ≤ Real.exp x ↔ 0 ≤ x

theorem Real.cosh_pos (x : ℝ) : 0 < Real.cosh x

Real.cosh is always positive

theorem Real.sinh_lt_cosh (x : ℝ) : Real.sinh x < Real.cosh x

theorem Complex.sum_div_factorial_le {α : Type u_1} [LinearOrderedField α] (n : ℕ) (j : ℕ) (hn : 0 < n) : (Finset.sum (Finset.filter (fun k => n ≤ k) (Finset.range j)) fun m => 1 / ↑(Nat.factorial m)) ≤ ↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n)

theorem Complex.exp_bound {x : ℂ} (hx : ↑Complex.abs x ≤ 1) {n : ℕ} (hn : 0 < n) : ↑Complex.abs (Complex.exp x - Finset.sum (Finset.range n) fun m => x ^ m / ↑(Nat.factorial m)) ≤ ↑Complex.abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)

theorem Complex.exp_bound' {x : ℂ} {n : ℕ} (hx : ↑Complex.abs x / ↑(Nat.succ n) ≤ 1 / 2) : ↑Complex.abs (Complex.exp x - Finset.sum (Finset.range n) fun m => x ^ m / ↑(Nat.factorial m)) ≤ ↑Complex.abs x ^ n / ↑(Nat.factorial n) * 2

theorem Complex.abs_exp_sub_one_le {x : ℂ} (hx : ↑Complex.abs x ≤ 1) : ↑Complex.abs (Complex.exp x - 1) ≤ 2 * ↑Complex.abs x

theorem Complex.abs_exp_sub_one_sub_id_le {x : ℂ} (hx : ↑Complex.abs x ≤ 1) : ↑Complex.abs (Complex.exp x - 1 - x) ≤ ↑Complex.abs x ^ 2

theorem Real.exp_bound {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) : |Real.exp x - Finset.sum (Finset.range n) fun m => x ^ m / ↑(Nat.factorial m)| ≤ |x| ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))

theorem Real.exp_bound' {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) {n : ℕ} (hn : 0 < n) : Real.exp x ≤ (Finset.sum (Finset.range n) fun m => x ^ m / ↑(Nat.factorial m)) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)

theorem Real.abs_exp_sub_one_le {x : ℝ} (hx : |x| ≤ 1) : |Real.exp x - 1| ≤ 2 * |x|

theorem Real.abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) : |Real.exp x - 1 - x| ≤ x ^ 2

noncomputable def Real.expNear (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 expNear_succ), with expNear n x r ⟶ exp x as n ⟶ ∞, for any r.

@[simp]

theorem Real.expNear_zero (x : ℝ) (r : ℝ) : Real.expNear 0 x r = r

@[simp]

theorem Real.expNear_succ (n : ℕ) (x : ℝ) (r : ℝ) : Real.expNear (n + 1) x r = Real.expNear n x (1 + x / (↑n + 1) * r)

theorem Real.expNear_sub (n : ℕ) (x : ℝ) (r₁ : ℝ) (r₂ : ℝ) : Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / ↑(Nat.factorial n) * (r₁ - r₂)

theorem Real.exp_approx_end (n : ℕ) (m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) : |Real.exp x - Real.expNear m x 0| ≤ |x| ^ m / ↑(Nat.factorial m) * ((↑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.expNear m x a₂| ≤ |x| ^ m / ↑(Nat.factorial m) * b₂) : |Real.exp x - Real.expNear n x a₁| ≤ |x| ^ n / ↑(Nat.factorial n) * 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)) : |Real.exp x - Real.expNear n x a| ≤ |x| ^ n / ↑(Nat.factorial n) * b

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

theorem Real.exp_approx_start (x : ℝ) (a : ℝ) (b : ℝ) (h : |Real.exp x - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b) : |Real.exp x - a| ≤ 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) : 0 < Real.cos x

theorem Real.sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < Real.sin x

theorem Real.sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < Real.sin x

theorem Real.cos_one_le : Real.cos 1 ≤ 2 / 3

theorem Real.cos_one_pos : 0 < Real.cos 1

theorem Real.cos_two_neg : Real.cos 2 < 0

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)

def Mathlib.Meta.Positivity.evalExp : Mathlib.Meta.Positivity.PositivityExt

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

@[simp]

theorem Complex.abs_cos_add_sin_mul_I (x : ℝ) : ↑Complex.abs (Complex.cos ↑x + Complex.sin ↑x * Complex.I) = 1

@[simp]

theorem Complex.abs_exp_ofReal (x : ℝ) : ↑Complex.abs (Complex.exp ↑x) = Real.exp x

@[simp]

theorem Complex.abs_exp_ofReal_mul_I (x : ℝ) : ↑Complex.abs (Complex.exp (↑x * Complex.I)) = 1

theorem Complex.abs_exp (z : ℂ) : ↑Complex.abs (Complex.exp z) = Real.exp z.re

theorem Complex.abs_exp_eq_iff_re_eq {x : ℂ} {y : ℂ} : ↑Complex.abs (Complex.exp x) = ↑Complex.abs (Complex.exp y) ↔ x.re = y.re