Trigonometric and hyperbolic trigonometric functions

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

noncomputable def Complex.sin (z : ℂ) : ℂ

The complex sine function, defined via exp

noncomputable def Complex.cos (z : ℂ) : ℂ

The complex cosine function, defined via exp

noncomputable def Complex.tan (z : ℂ) : ℂ

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

noncomputable def Complex.cot (z : ℂ) : ℂ

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

noncomputable def Complex.sinh (z : ℂ) : ℂ

The complex hyperbolic sine function, defined via exp

noncomputable def Complex.cosh (z : ℂ) : ℂ

The complex hyperbolic cosine function, defined via exp

noncomputable def Complex.tanh (z : ℂ) : ℂ

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

noncomputable def Real.sin (x : ℝ) : ℝ

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

noncomputable def Real.cos (x : ℝ) : ℝ

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

noncomputable def Real.tan (x : ℝ) : ℝ

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

noncomputable def Real.cot (x : ℝ) : ℝ

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

noncomputable def Real.sinh (x : ℝ) : ℝ

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

noncomputable def Real.cosh (x : ℝ) : ℝ

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

noncomputable def Real.tanh (x : ℝ) : ℝ

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

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

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

@[simp]

theorem Complex.sinh_zero : sinh 0 = 0

@[simp]

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

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

@[simp]

theorem Complex.cosh_zero : cosh 0 = 1

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Complex.tanh_zero : tanh 0 = 0

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

theorem Complex.sin_zero : sin 0 = 0

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Complex.cos_zero : cos 0 = 1

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Complex.tan_zero : tan 0 = 0

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

theorem Complex.cot_eq_cos_div_sin (x : ℂ) : x.cot = cos x / sin x

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

@[simp]

theorem Complex.tan_inv_eq_cot (x : ℂ) : (tan x)⁻¹ = x.cot

@[simp]

theorem Complex.cot_inv_eq_tan (x : ℂ) : x.cot⁻¹ = tan x

@[simp]

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

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

theorem Complex.cot_conj (x : ℂ) : ((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot

@[simp]

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

@[simp]

theorem Complex.ofReal_cot_ofReal_re (x : ℝ) : ↑(↑x).cot.re = (↑x).cot

@[simp]

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

@[simp]

theorem Complex.ofReal_cot (x : ℝ) : ↑x.cot = (↑x).cot

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

theorem Complex.one_add_tan_sq_mul_cos_sq_eq_one {x : ℂ} (h : cos x ≠ 0) : (1 + tan x ^ 2) * cos x ^ 2 = 1

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem Complex.exp_ofReal_mul_I (x : ℝ) : exp (↑x * I) = ↑(Real.cos x) + ↑(Real.sin x) * I

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

De Moivre's formula

theorem Complex.cos_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖cos x - (1 - x ^ 2 / 2)‖ ≤ ‖x‖ ^ 4 * (5 / 96)

theorem Complex.sin_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖sin x - (x - x ^ 3 / 6)‖ ≤ ‖x‖ ^ 4 * (5 / 96)

@[simp]

theorem Real.sin_zero : sin 0 = 0

@[simp]

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

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

@[simp]

theorem Real.cos_zero : cos 0 = 1

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.cot_eq_cos_div_sin (x : ℝ) : x.cot = cos x / sin x

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

@[simp]

theorem Real.tan_inv_eq_cot (x : ℝ) : (tan x)⁻¹ = x.cot

@[simp]

theorem Real.cot_inv_eq_tan (x : ℝ) : x.cot⁻¹ = tan x

@[simp]

theorem Real.tan_zero : tan 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.one_add_tan_sq_mul_cos_sq_eq_one {x : ℝ} (h : cos x ≠ 0) : (1 + tan x ^ 2) * cos x ^ 2 = 1

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

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

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

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

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

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

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

The definition of sinh in terms of exp.

@[simp]

theorem Real.sinh_zero : sinh 0 = 0

@[simp]

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

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

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

The definition of cosh in terms of exp.

@[simp]

theorem Real.cosh_zero : cosh 0 = 1

@[simp]

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

@[simp]

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

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

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

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

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

theorem Real.tanh_eq (x : ℝ) : tanh x = (exp x - exp (-x)) / (exp x + exp (-x))

The definition of tanh in terms of exp.

@[simp]

theorem Real.tanh_zero : tanh 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

Real.cosh is always positive

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

theorem Real.tanh_lt_one (x : ℝ) : tanh x < 1

theorem Real.neg_one_lt_tanh (x : ℝ) : -1 < tanh x

theorem Real.abs_tanh_lt_one (x : ℝ) : |tanh x| < 1

theorem Real.tanh_sq_lt_one (x : ℝ) : tanh x ^ 2 < 1

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

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

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

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

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

theorem Real.cos_one_le : cos 1 ≤ 5 / 9

theorem Real.cos_one_pos : 0 < cos 1

theorem Real.cos_two_neg : cos 2 < 0

def Mathlib.Meta.Positivity.evalCosh : PositivityExt

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

@[simp]

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

@[simp]

theorem Complex.norm_exp_ofReal_mul_I (x : ℝ) : ‖exp (↑x * I)‖ = 1

@[simp]

theorem Complex.norm_exp_I_mul_ofReal (x : ℝ) : ‖exp (I * ↑x)‖ = 1

@[simp]

theorem Complex.nnnorm_exp_ofReal_mul_I (x : ℝ) : ‖exp (↑x * I)‖₊ = 1

@[simp]

theorem Complex.nnnorm_exp_I_mul_ofReal (x : ℝ) : ‖exp (I * ↑x)‖₊ = 1

@[simp]

theorem Complex.enorm_exp_ofReal_mul_I (x : ℝ) : ‖exp (↑x * I)‖ₑ = 1

@[simp]

theorem Complex.enorm_exp_I_mul_ofReal (x : ℝ) : ‖exp (I * ↑x)‖ₑ = 1

theorem Complex.norm_exp_I_mul_ofReal_sub_one (x : ℝ) : ‖exp (I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

theorem Complex.norm_exp (z : ℂ) : ‖exp z‖ = Real.exp z.re

theorem Complex.norm_exp_eq_iff_re_eq {x y : ℂ} : ‖exp x‖ = ‖exp y‖ ↔ x.re = y.re