# mathlib3documentation

analysis.special_functions.trigonometric.basic

# Trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

This file contains the definition of π.

See also analysis.special_functions.trigonometric.inverse and analysis.special_functions.trigonometric.arctan for the inverse trigonometric functions.

See also analysis.special_functions.complex.arg and analysis.special_functions.complex.log for the complex argument function and the complex logarithm.

## Main statements #

Many basic inequalities on the real trigonometric functions are established.

The continuity of the usual trigonometric functions is proved.

Several facts about the real trigonometric functions have the proofs deferred to analysis.special_functions.trigonometric.complex, as they are most easily proved by appealing to the corresponding fact for complex trigonometric functions.

See also analysis.special_functions.trigonometric.chebyshev for the multiple angle formulas in terms of Chebyshev polynomials.

## Tags #

sin, cos, tan, angle

@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[protected]
noncomputable def real.pi  :

The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from which one can derive all its properties. For explicit bounds on π, see data.real.pi.bounds.

Equations
@[simp]
theorem real.cos_pi_div_two  :
theorem real.two_le_pi  :
theorem real.pi_le_four  :
theorem real.pi_pos  :
theorem real.pi_ne_zero  :
theorem real.pi_div_two_pos  :
0 <
theorem real.two_pi_pos  :
0 <
noncomputable def nnreal.pi  :

π considered as a nonnegative real.

Equations
@[simp]
theorem nnreal.coe_real_pi  :
theorem nnreal.pi_pos  :
@[simp]
theorem real.sin_pi  :
@[simp]
theorem real.cos_pi  :
@[simp]
theorem real.sin_two_pi  :
@[simp]
theorem real.cos_two_pi  :
@[simp]
theorem real.sin_add_pi (x : ) :
@[simp]
theorem real.sin_add_two_pi (x : ) :
@[simp]
theorem real.sin_sub_pi (x : ) :
@[simp]
theorem real.sin_sub_two_pi (x : ) :
@[simp]
theorem real.sin_pi_sub (x : ) :
@[simp]
theorem real.sin_two_pi_sub (x : ) :
@[simp]
theorem real.sin_nat_mul_pi (n : ) :
@[simp]
theorem real.sin_int_mul_pi (n : ) :
@[simp]
theorem real.sin_add_nat_mul_two_pi (x : ) (n : ) :
real.sin (x + n * (2 * real.pi)) =
@[simp]
theorem real.sin_add_int_mul_two_pi (x : ) (n : ) :
real.sin (x + n * (2 * real.pi)) =
@[simp]
theorem real.sin_sub_nat_mul_two_pi (x : ) (n : ) :
real.sin (x - n * (2 * real.pi)) =
@[simp]
theorem real.sin_sub_int_mul_two_pi (x : ) (n : ) :
real.sin (x - n * (2 * real.pi)) =
@[simp]
theorem real.sin_nat_mul_two_pi_sub (x : ) (n : ) :
real.sin (n * (2 * real.pi) - x) =
@[simp]
theorem real.sin_int_mul_two_pi_sub (x : ) (n : ) :
real.sin (n * (2 * real.pi) - x) =
@[simp]
theorem real.cos_add_pi (x : ) :
@[simp]
theorem real.cos_add_two_pi (x : ) :
@[simp]
theorem real.cos_sub_pi (x : ) :
@[simp]
theorem real.cos_sub_two_pi (x : ) :
@[simp]
theorem real.cos_pi_sub (x : ) :
@[simp]
theorem real.cos_two_pi_sub (x : ) :
@[simp]
theorem real.cos_nat_mul_two_pi (n : ) :
real.cos (n * (2 * real.pi)) = 1
@[simp]
theorem real.cos_int_mul_two_pi (n : ) :
real.cos (n * (2 * real.pi)) = 1
@[simp]
theorem real.cos_add_nat_mul_two_pi (x : ) (n : ) :
real.cos (x + n * (2 * real.pi)) =
@[simp]
theorem real.cos_add_int_mul_two_pi (x : ) (n : ) :
real.cos (x + n * (2 * real.pi)) =
@[simp]
theorem real.cos_sub_nat_mul_two_pi (x : ) (n : ) :
real.cos (x - n * (2 * real.pi)) =
@[simp]
theorem real.cos_sub_int_mul_two_pi (x : ) (n : ) :
real.cos (x - n * (2 * real.pi)) =
@[simp]
theorem real.cos_nat_mul_two_pi_sub (x : ) (n : ) :
real.cos (n * (2 * real.pi) - x) =
@[simp]
theorem real.cos_int_mul_two_pi_sub (x : ) (n : ) :
real.cos (n * (2 * real.pi) - x) =
@[simp]
@[simp]
@[simp]
@[simp]
theorem real.sin_pos_of_pos_of_lt_pi {x : } (h0x : 0 < x) (hxp : x < real.pi) :
0 <
theorem real.sin_pos_of_mem_Ioo {x : } (hx : x ) :
0 <
theorem real.sin_nonneg_of_mem_Icc {x : } (hx : x ) :
0
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : } (h0x : 0 x) (hxp : x real.pi) :
0
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : } (hx0 : x < 0) (hpx : -real.pi < x) :
< 0
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : } (hx0 : x 0) (hpx : -real.pi x) :
0
@[simp]
theorem real.sin_pi_div_two  :
theorem real.cos_pos_of_mem_Ioo {x : } (hx : x set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
0 <
theorem real.cos_nonneg_of_mem_Icc {x : } (hx : x set.Icc (-(real.pi / 2)) (real.pi / 2)) :
0
theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : } (hl : -(real.pi / 2) x) (hu : x ) :
0
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : } (hx₁ : < x) (hx₂ : x < ) :
< 0
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } (hx₁ : x) (hx₂ : x ) :
0
theorem real.sin_eq_sqrt_one_sub_cos_sq {x : } (hl : 0 x) (hu : x real.pi) :
= (1 - ^ 2)
theorem real.cos_eq_sqrt_one_sub_sin_sq {x : } (hl : -(real.pi / 2) x) (hu : x ) :
= (1 - ^ 2)
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : } (hx₁ : -real.pi < x) (hx₂ : x < real.pi) :
= 0 x = 0
theorem real.sin_eq_zero_iff {x : } :
= 0 (n : ), = x
theorem real.sin_ne_zero_iff {x : } :
0 (n : ), x
theorem real.sin_eq_zero_iff_cos_eq {x : } :
= 0 = 1 = -1
theorem real.cos_eq_one_iff (x : ) :
= 1 (n : ), n * (2 * real.pi) = x
theorem real.cos_eq_one_iff_of_lt_of_lt {x : } (hx₁ : -(2 * real.pi) < x) (hx₂ : x < ) :
= 1 x = 0
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y ) (hxy : x < y) :
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y real.pi) (hxy : x < y) :
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y real.pi) (hxy : x y) :
theorem real.sin_lt_sin_of_lt_of_le_pi_div_two {x y : } (hx₁ : -(real.pi / 2) x) (hy₂ : y ) (hxy : x < y) :
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : } (hx₁ : -(real.pi / 2) x) (hy₂ : y ) (hxy : x y) :
theorem real.inj_on_sin  :
(set.Icc (-(real.pi / 2)) (real.pi / 2))
theorem real.inj_on_cos  :
theorem real.surj_on_sin  :
(set.Icc (-(real.pi / 2)) (real.pi / 2)) (set.Icc (-1) 1)
theorem real.surj_on_cos  :
(set.Icc (-1) 1)
theorem real.sin_mem_Icc (x : ) :
set.Icc (-1) 1
theorem real.cos_mem_Icc (x : ) :
set.Icc (-1) 1
theorem real.maps_to_sin (s : set ) :
(set.Icc (-1) 1)
theorem real.maps_to_cos (s : set ) :
(set.Icc (-1) 1)
theorem real.bij_on_sin  :
(set.Icc (-(real.pi / 2)) (real.pi / 2)) (set.Icc (-1) 1)
theorem real.bij_on_cos  :
(set.Icc (-1) 1)
@[simp]
theorem real.range_cos  :
= set.Icc (-1) 1
@[simp]
theorem real.range_sin  :
= set.Icc (-1) 1
@[simp]
noncomputable def real.sqrt_two_add_series (x : ) :

the series sqrt_two_add_series x n is sqrt(2 + sqrt(2 + ... )) with n square roots, starting with x. We define it here because cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2

Equations
theorem real.sqrt_two_add_series_nonneg {x : } (h : 0 x) (n : ) :
theorem real.sqrt_two_add_series_succ (x : ) (n : ) :
(n + 1) = real.sqrt_two_add_series ( (2 + x)) n
theorem real.sqrt_two_add_series_monotone_left {x y : } (h : x y) (n : ) :
@[simp]
theorem real.cos_pi_over_two_pow (n : ) :
real.cos (real.pi / 2 ^ (n + 1)) =
theorem real.sin_sq_pi_over_two_pow (n : ) :
real.sin (real.pi / 2 ^ (n + 1)) ^ 2 = 1 - / 2) ^ 2
theorem real.sin_sq_pi_over_two_pow_succ (n : ) :
real.sin (real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 -
@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ) :
real.sin (real.pi / 2 ^ (n + 2)) = (2 - / 2
@[simp]
theorem real.cos_pi_div_four  :
@[simp]
theorem real.sin_pi_div_four  :
@[simp]
theorem real.cos_pi_div_eight  :
real.cos (real.pi / 8) = (2 + 2) / 2
@[simp]
theorem real.sin_pi_div_eight  :
real.sin (real.pi / 8) = (2 - 2) / 2
@[simp]
theorem real.cos_pi_div_sixteen  :
real.cos (real.pi / 16) = (2 + (2 + 2)) / 2
@[simp]
theorem real.sin_pi_div_sixteen  :
real.sin (real.pi / 16) = (2 - (2 + 2)) / 2
@[simp]
theorem real.cos_pi_div_thirty_two  :
real.cos (real.pi / 32) = (2 + (2 + (2 + 2))) / 2
@[simp]
theorem real.sin_pi_div_thirty_two  :
real.sin (real.pi / 32) = (2 - (2 + (2 + 2))) / 2
@[simp]
theorem real.cos_pi_div_three  :
real.cos (real.pi / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

theorem real.sq_cos_pi_div_six  :
real.cos (real.pi / 6) ^ 2 = 3 / 4

The square of the cosine of π / 6 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

@[simp]
theorem real.cos_pi_div_six  :

The cosine of π / 6 is √3 / 2.

@[simp]
theorem real.sin_pi_div_six  :
real.sin (real.pi / 6) = 1 / 2

The sine of π / 6 is 1 / 2.

theorem real.sq_sin_pi_div_three  :
real.sin (real.pi / 3) ^ 2 = 3 / 4

The square of the sine of π / 3 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

@[simp]
theorem real.sin_pi_div_three  :

The sine of π / 3 is √3 / 2.

noncomputable def real.sin_order_iso  :

real.sin as an order_iso between [-(π / 2), π / 2] and [-1, 1].

Equations
@[simp]
theorem real.sin_order_iso_apply (x : (set.Icc (-(real.pi / 2)) (real.pi / 2))) :
= , _⟩
@[simp]
@[simp]
theorem real.tan_pi_div_two  :
theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : } (h0x : 0 < x) (hxp : x < ) :
0 <
theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : } (h0x : 0 x) (hxp : x ) :
0
theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : } (hx0 : x < 0) (hpx : -(real.pi / 2) < x) :
< 0
theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : } (hx0 : x 0) (hpx : -(real.pi / 2) x) :
0
theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y < ) (hxy : x < y) :
theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(real.pi / 2) < x) (hy₂ : y < ) (hxy : x < y) :
theorem real.inj_on_tan  :
(set.Ioo (-(real.pi / 2)) (real.pi / 2))
theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(real.pi / 2) < x) (hx₂ : x < ) (hy₁ : -(real.pi / 2) < y) (hy₂ : y < ) (hxy : = ) :
x = y
theorem real.tan_add_pi (x : ) :
theorem real.tan_sub_pi (x : ) :
theorem real.tan_pi_sub (x : ) :
theorem real.tan_add_nat_mul_pi (x : ) (n : ) :
theorem real.tan_add_int_mul_pi (x : ) (n : ) :
theorem real.tan_sub_nat_mul_pi (x : ) (n : ) :
theorem real.tan_sub_int_mul_pi (x : ) (n : ) :
theorem real.tan_nat_mul_pi_sub (x : ) (n : ) :
theorem real.tan_int_mul_pi_sub (x : ) (n : ) :
theorem complex.sin_eq_zero_iff_cos_eq {z : } :
= 0 = 1 = -1
@[simp]
theorem complex.sin_pi  :
@[simp]
theorem complex.cos_pi  :
@[simp]
@[simp]
theorem complex.sin_add_pi (x : ) :
theorem complex.sin_sub_pi (x : ) :
theorem complex.sin_nat_mul_pi (n : ) :
= 0
theorem complex.sin_int_mul_pi (n : ) :
= 0
theorem complex.cos_add_pi (x : ) :
theorem complex.cos_sub_pi (x : ) :
theorem complex.cos_pi_sub (x : ) :
theorem complex.tan_pi_sub (x : ) :
theorem complex.tan_nat_mul_pi (n : ) :
= 0
theorem complex.tan_int_mul_pi (n : ) :
= 0
theorem complex.tan_add_nat_mul_pi (x : ) (n : ) :
theorem complex.tan_add_int_mul_pi (x : ) (n : ) :
theorem complex.tan_sub_nat_mul_pi (x : ) (n : ) :
theorem complex.tan_sub_int_mul_pi (x : ) (n : ) :
theorem complex.tan_nat_mul_pi_sub (x : ) (n : ) :
theorem complex.tan_int_mul_pi_sub (x : ) (n : ) :
@[simp]
theorem complex.exp_pi_mul_I  :
= -1
@[simp]
@[simp]
@[simp]
@[simp]
theorem complex.exp_add_pi_mul_I (z : ) :
cexp (z + = -cexp z
@[simp]
theorem complex.exp_sub_pi_mul_I (z : ) :
cexp (z - = -cexp z
theorem complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le {a b : } (ha : a 0) {z : } (hz : |z.im| b) (hb : b ) :

A supporting lemma for the Phragmen-Lindelöf principle in a horizontal strip. If z : ℂ belongs to a horizontal strip |complex.im z| ≤ b, b ≤ π / 2, and a ≤ 0, then $$\left|exp^{a\left(e^{z}+e^{-z}\right)}\right| \le e^{a\cos b \exp^{|re z|}}.$$