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 Complex.isCauSeq_abs_exp (z : ℂ) : IsCauSeq abs fun (n : ℕ) => (Finset.range n).sum fun (m : ℕ) => Complex.abs (z ^ m / ↑m.factorial)

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

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

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

Equations

• z.exp' = ⟨fun (n : ℕ) => (Finset.range n).sum fun (m : ℕ) => z ^ m / ↑m.factorial, ⋯⟩

def Complex.exp (z : ℂ) : ℂ

The complex exponential function, defined via its Taylor series

Equations

• z.exp = z.exp'.lim

def Complex.sin (z : ℂ) : ℂ

The complex sine function, defined via exp

Equations

• z.sin = ((-z * Complex.I).exp - (z * Complex.I).exp) * Complex.I / 2

def Complex.cos (z : ℂ) : ℂ

The complex cosine function, defined via exp

Equations

• z.cos = ((z * Complex.I).exp + (-z * Complex.I).exp) / 2

def Complex.tan (z : ℂ) : ℂ

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

Equations

• z.tan = z.sin / z.cos

def Complex.sinh (z : ℂ) : ℂ

The complex hyperbolic sine function, defined via exp

Equations

• z.sinh = (z.exp - (-z).exp) / 2

def Complex.cosh (z : ℂ) : ℂ

The complex hyperbolic cosine function, defined via exp

Equations

• z.cosh = (z.exp + (-z).exp) / 2

def Complex.tanh (z : ℂ) : ℂ

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

Equations

• z.tanh = z.sinh / z.cosh

def Complex.termCexp : Lean.ParserDescr

scoped notation for the complex exponential function

Equations

• Complex.termCexp = Lean.ParserDescr.node `Complex.termCexp 1024 (Lean.ParserDescr.symbol "cexp")

def Real.exp (x : ℝ) : ℝ

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

Equations

• x.exp = (↑x).exp.re

def Real.sin (x : ℝ) : ℝ

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

Equations

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

def Real.cos (x : ℝ) : ℝ

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

Equations

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

def Real.tan (x : ℝ) : ℝ

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

Equations

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

def Real.sinh (x : ℝ) : ℝ

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

Equations

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

def Real.cosh (x : ℝ) : ℝ

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

Equations

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

def Real.tanh (x : ℝ) : ℝ

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

Equations

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

def Real.termRexp : Lean.ParserDescr

scoped notation for the real exponential function

Equations

• Real.termRexp = Lean.ParserDescr.node `Real.termRexp 1024 (Lean.ParserDescr.symbol "rexp")

@[simp]

theorem Complex.exp_zero : Complex.exp 0 = 1

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

noncomputable def Complex.expMonoidHom : Multiplicative ℂ →* ℂ

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

Equations

• Complex.expMonoidHom = { toFun := fun (z : Multiplicative ℂ) => (Multiplicative.toAdd z).exp, map_one' := Complex.expMonoidHom.proof_1, map_mul' := Complex.expMonoidHom.proof_2 }

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

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

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

theorem Complex.exp_nsmul (x : ℂ) (n : ℕ) : (n • x).exp = x.exp ^ n

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem Complex.sinh_zero : Complex.sinh 0 = 0

@[simp]

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

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

@[simp]

theorem Complex.cosh_zero : Complex.cosh 0 = 1

@[simp]

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

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

theorem Complex.sinh_sub (x : ℂ) (y : ℂ) : (x - y).sinh = x.sinh * y.cosh - x.cosh * y.sinh

theorem Complex.cosh_sub (x : ℂ) (y : ℂ) : (x - y).cosh = x.cosh * y.cosh - x.sinh * y.sinh

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Complex.tanh_zero : Complex.tanh 0 = 0

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

theorem Complex.sin_zero : Complex.sin 0 = 0

@[simp]

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

theorem Complex.two_sin (x : ℂ) : 2 * x.sin = ((-x * Complex.I).exp - (x * Complex.I).exp) * Complex.I

theorem Complex.two_cos (x : ℂ) : 2 * x.cos = (x * Complex.I).exp + (-x * Complex.I).exp

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

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

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

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

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

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

theorem Complex.sin_add (x : ℂ) (y : ℂ) : (x + y).sin = x.sin * y.cos + x.cos * y.sin

@[simp]

theorem Complex.cos_zero : Complex.cos 0 = 1

@[simp]

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

theorem Complex.cos_add (x : ℂ) (y : ℂ) : (x + y).cos = x.cos * y.cos - x.sin * y.sin

theorem Complex.sin_sub (x : ℂ) (y : ℂ) : (x - y).sin = x.sin * y.cos - x.cos * y.sin

theorem Complex.cos_sub (x : ℂ) (y : ℂ) : (x - y).cos = x.cos * y.cos + x.sin * y.sin

theorem Complex.sin_add_mul_I (x : ℂ) (y : ℂ) : (x + y * Complex.I).sin = x.sin * y.cosh + x.cos * y.sinh * Complex.I

theorem Complex.sin_eq (z : ℂ) : z.sin = (↑z.re).sin * (↑z.im).cosh + (↑z.re).cos * (↑z.im).sinh * Complex.I

theorem Complex.cos_add_mul_I (x : ℂ) (y : ℂ) : (x + y * Complex.I).cos = x.cos * y.cosh - x.sin * y.sinh * Complex.I

theorem Complex.cos_eq (z : ℂ) : z.cos = (↑z.re).cos * (↑z.im).cosh - (↑z.re).sin * (↑z.im).sinh * Complex.I

theorem Complex.sin_sub_sin (x : ℂ) (y : ℂ) : x.sin - y.sin = 2 * ((x - y) / 2).sin * ((x + y) / 2).cos

theorem Complex.cos_sub_cos (x : ℂ) (y : ℂ) : x.cos - y.cos = -2 * ((x + y) / 2).sin * ((x - y) / 2).sin

theorem Complex.cos_add_cos (x : ℂ) (y : ℂ) : x.cos + y.cos = 2 * ((x + y) / 2).cos * ((x - y) / 2).cos

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Complex.tan_zero : Complex.tan 0 = 0

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Complex.cos_add_sin_I (x : ℂ) : x.cos + x.sin * Complex.I = (x * Complex.I).exp

theorem Complex.cos_sub_sin_I (x : ℂ) : x.cos - x.sin * Complex.I = (-x * Complex.I).exp

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

theorem Complex.tan_sq_div_one_add_tan_sq {x : ℂ} (hx : x.cos ≠ 0) : x.tan ^ 2 / (1 + x.tan ^ 2) = x.sin ^ 2

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

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

theorem Complex.exp_mul_I (x : ℂ) : (x * Complex.I).exp = x.cos + x.sin * Complex.I

theorem Complex.exp_add_mul_I (x : ℂ) (y : ℂ) : (x + y * Complex.I).exp = x.exp * (y.cos + y.sin * Complex.I)

theorem Complex.exp_eq_exp_re_mul_sin_add_cos (x : ℂ) : x.exp = (↑x.re).exp * ((↑x.im).cos + (↑x.im).sin * Complex.I)

theorem Complex.exp_re (x : ℂ) : x.exp.re = x.re.exp * x.im.cos

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

@[simp]

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

@[simp]

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

theorem Complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (z.cos + z.sin * Complex.I) ^ n = (↑n * z).cos + (↑n * z).sin * Complex.I

De Moivre's formula

@[simp]

theorem Real.exp_zero : Real.exp 0 = 1

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

noncomputable def Real.expMonoidHom : Multiplicative ℝ →* ℝ

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

Equations

• Real.expMonoidHom = { toFun := fun (x : Multiplicative ℝ) => (Multiplicative.toAdd x).exp, map_one' := Real.expMonoidHom.proof_1, map_mul' := Real.expMonoidHom.proof_2 }

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

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

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

theorem Real.exp_nsmul (x : ℝ) (n : ℕ) : (n • x).exp = x.exp ^ n

theorem Real.exp_nat_mul (x : ℝ) (n : ℕ) : (↑n * x).exp = x.exp ^ n

theorem Real.exp_ne_zero (x : ℝ) : x.exp ≠ 0

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

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

@[simp]

theorem Real.sin_zero : Real.sin 0 = 0

@[simp]

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

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

@[simp]

theorem Real.cos_zero : Real.cos 0 = 1

@[simp]

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

@[simp]

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

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

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

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

theorem Real.sin_sub_sin (x : ℝ) (y : ℝ) : x.sin - y.sin = 2 * ((x - y) / 2).sin * ((x + y) / 2).cos

theorem Real.cos_sub_cos (x : ℝ) (y : ℝ) : x.cos - y.cos = -2 * ((x + y) / 2).sin * ((x - y) / 2).sin

theorem Real.cos_add_cos (x : ℝ) (y : ℝ) : x.cos + y.cos = 2 * ((x + y) / 2).cos * ((x - y) / 2).cos

theorem Real.tan_eq_sin_div_cos (x : ℝ) : x.tan = x.sin / x.cos

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

@[simp]

theorem Real.tan_zero : Real.tan 0 = 0

@[simp]

theorem Real.tan_neg (x : ℝ) : (-x).tan = -x.tan

@[simp]

theorem Real.sin_sq_add_cos_sq (x : ℝ) : x.sin ^ 2 + x.cos ^ 2 = 1

@[simp]

theorem Real.cos_sq_add_sin_sq (x : ℝ) : x.cos ^ 2 + x.sin ^ 2 = 1

theorem Real.sin_sq_le_one (x : ℝ) : x.sin ^ 2 ≤ 1

theorem Real.cos_sq_le_one (x : ℝ) : x.cos ^ 2 ≤ 1

theorem Real.abs_sin_le_one (x : ℝ) : |x.sin| ≤ 1

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

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

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

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

theorem Real.neg_one_le_cos (x : ℝ) : -1 ≤ x.cos

theorem Real.cos_two_mul (x : ℝ) : (2 * x).cos = 2 * x.cos ^ 2 - 1

theorem Real.cos_two_mul' (x : ℝ) : (2 * x).cos = x.cos ^ 2 - x.sin ^ 2

theorem Real.sin_two_mul (x : ℝ) : (2 * x).sin = 2 * x.sin * x.cos

theorem Real.cos_sq (x : ℝ) : x.cos ^ 2 = 1 / 2 + (2 * x).cos / 2

theorem Real.cos_sq' (x : ℝ) : x.cos ^ 2 = 1 - x.sin ^ 2

theorem Real.sin_sq (x : ℝ) : x.sin ^ 2 = 1 - x.cos ^ 2

theorem Real.sin_sq_eq_half_sub (x : ℝ) : x.sin ^ 2 = 1 / 2 - (2 * x).cos / 2

theorem Real.abs_sin_eq_sqrt_one_sub_cos_sq (x : ℝ) : |x.sin| = (1 - x.cos ^ 2).sqrt

theorem Real.abs_cos_eq_sqrt_one_sub_sin_sq (x : ℝ) : |x.cos| = (1 - x.sin ^ 2).sqrt

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

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

theorem Real.inv_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < x.cos) : (1 + x.tan ^ 2).sqrt⁻¹ = x.cos

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

theorem Real.cos_three_mul (x : ℝ) : (3 * x).cos = 4 * x.cos ^ 3 - 3 * x.cos

theorem Real.sin_three_mul (x : ℝ) : (3 * x).sin = 3 * x.sin - 4 * x.sin ^ 3

theorem Real.sinh_eq (x : ℝ) : x.sinh = (x.exp - (-x).exp) / 2

The definition of sinh in terms of exp.

@[simp]

theorem Real.sinh_zero : Real.sinh 0 = 0

@[simp]

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

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

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

The definition of cosh in terms of exp.

@[simp]

theorem Real.cosh_zero : Real.cosh 0 = 1

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem Real.tanh_zero : Real.tanh 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.cosh_sq_sub_sinh_sq (x : ℝ) : x.cosh ^ 2 - x.sinh ^ 2 = 1

theorem Real.cosh_sq (x : ℝ) : x.cosh ^ 2 = x.sinh ^ 2 + 1

theorem Real.cosh_sq' (x : ℝ) : x.cosh ^ 2 = 1 + x.sinh ^ 2

theorem Real.sinh_sq (x : ℝ) : x.sinh ^ 2 = x.cosh ^ 2 - 1

theorem Real.cosh_two_mul (x : ℝ) : (2 * x).cosh = x.cosh ^ 2 + x.sinh ^ 2

theorem Real.sinh_two_mul (x : ℝ) : (2 * x).sinh = 2 * x.sinh * x.cosh

theorem Real.cosh_three_mul (x : ℝ) : (3 * x).cosh = 4 * x.cosh ^ 3 - 3 * x.cosh

theorem Real.sinh_three_mul (x : ℝ) : (3 * x).sinh = 4 * x.sinh ^ 3 + 3 * x.sinh

theorem Real.sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ((Finset.range n).sum fun (i : ℕ) => x ^ i / ↑i.factorial) ≤ x.exp

theorem Real.pow_div_factorial_le_exp (x : ℝ) (hx : 0 ≤ x) (n : ℕ) : x ^ n / ↑n.factorial ≤ x.exp

theorem Real.quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2 ≤ x.exp

theorem Real.one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ x.exp

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

theorem Real.exp_nonneg (x : ℝ) : 0 ≤ x.exp

@[simp]

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

theorem Real.exp_abs_le (x : ℝ) : |x|.exp ≤ x.exp + (-x).exp

theorem Real.exp_strictMono : StrictMono Real.exp

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

theorem Real.exp_monotone : Monotone Real.exp

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

@[simp]

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

@[simp]

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

theorem Real.exp_injective : Function.Injective Real.exp

@[simp]

theorem Real.exp_eq_exp {x : ℝ} {y : ℝ} : x.exp = y.exp ↔ x = y

@[simp]

theorem Real.exp_eq_one_iff (x : ℝ) : x.exp = 1 ↔ x = 0

@[simp]

theorem Real.one_lt_exp_iff {x : ℝ} : 1 < x.exp ↔ 0 < x

@[simp]

theorem Real.exp_lt_one_iff {x : ℝ} : x.exp < 1 ↔ x < 0

@[simp]

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

@[simp]

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

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

Real.cosh is always positive

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

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

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

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

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

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

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

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

theorem Real.abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) : |x.exp - 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.

Equations

• Real.expNear n x r = ((Finset.range n).sum fun (m : ℕ) => x ^ m / ↑m.factorial) + x ^ n / ↑n.factorial * 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 / ↑n.factorial * (r₁ - r₂)

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

theorem Real.exp_approx_start (x : ℝ) (a : ℝ) (b : ℝ) (h : |x.exp - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b) : |x.exp - a| ≤ b

theorem Real.cos_bound {x : ℝ} (hx : |x| ≤ 1) : |x.cos - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)

theorem Real.sin_bound {x : ℝ} (hx : |x| ≤ 1) : |x.sin - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96)

theorem Real.cos_pos_of_le_one {x : ℝ} (hx : |x| ≤ 1) : 0 < x.cos

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

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

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) : x.exp < 1 / (1 - x)

theorem Real.exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) : x.exp ≤ 1 / (1 - x)

theorem Real.add_one_lt_exp {x : ℝ} (hx : x ≠ 0) : x + 1 < x.exp

theorem Real.add_one_le_exp (x : ℝ) : x + 1 ≤ x.exp

theorem Real.one_sub_lt_exp_neg {x : ℝ} (hx : x ≠ 0) : 1 - x < (-x).exp

theorem Real.one_sub_le_exp_neg (x : ℝ) : 1 - x ≤ (-x).exp

theorem Real.one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ ↑n) : (1 - t / ↑n) ^ n ≤ (-t).exp

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

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

def Mathlib.Meta.Positivity.evalCosh : Mathlib.Meta.Positivity.PositivityExt

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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