mathlib3 documentation

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

source
@[continuity]
theorem complex.continuous_sin  :
continuous complex.sin
source
theorem complex.continuous_on_sin {s : set ℂ} :
continuous_on complex.sin s
source
@[continuity]
theorem complex.continuous_cos  :
continuous complex.cos
source
theorem complex.continuous_on_cos {s : set ℂ} :
continuous_on complex.cos s
source
@[continuity]
theorem complex.continuous_sinh  :
continuous complex.sinh
source
@[continuity]
theorem complex.continuous_cosh  :
continuous complex.cosh
source
@[continuity]
theorem real.continuous_sin  :
continuous real.sin
source
theorem real.continuous_on_sin {s : set ℝ} :
continuous_on real.sin s
source
@[continuity]
theorem real.continuous_cos  :
continuous real.cos
source
theorem real.continuous_on_cos {s : set ℝ} :
continuous_on real.cos s
source
@[continuity]
theorem real.continuous_sinh  :
continuous real.sinh
source
@[continuity]
theorem real.continuous_cosh  :
continuous real.cosh
source
theorem real.exists_cos_eq_zero  :
0 ∈ real.cos '' set.Icc 1 2
source
@[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
source
@[simp]
theorem real.cos_pi_div_two  :
real.cos (real.pi / 2) = 0
source
theorem real.one_le_pi_div_two  :
1 ≤ real.pi / 2
source
theorem real.pi_div_two_le_two  :
real.pi / 2 ≤ 2
source
theorem real.two_le_pi  :
2 ≤ real.pi
source
theorem real.pi_le_four  :
real.pi ≤ 4
source
theorem real.pi_pos  :
0 < real.pi
source
theorem real.pi_ne_zero  :
real.pi ≠ 0
source
theorem real.pi_div_two_pos  :
0 < real.pi / 2
source
theorem real.two_pi_pos  :
0 < 2 * real.pi
source
noncomputable def nnreal.pi  :
nnreal

π considered as a nonnegative real.

Equations
source
@[simp]
theorem nnreal.coe_real_pi  :
↑nnreal.pi = real.pi
source
theorem nnreal.pi_pos  :
0 < nnreal.pi
source
theorem nnreal.pi_ne_zero  :
nnreal.pi ≠ 0
source
@[simp]
theorem real.sin_pi  :
real.sin real.pi = 0
source
@[simp]
theorem real.cos_pi  :
real.cos real.pi = -1
source
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * real.pi) = 0
source
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * real.pi) = 1
source
theorem real.sin_antiperiodic  :
function.antiperiodic real.sin real.pi
source
theorem real.sin_periodic  :
function.periodic real.sin (2 * real.pi)
source
@[simp]
theorem real.sin_add_pi (x : ℝ) :
real.sin (x + real.pi) = -real.sin x
source
@[simp]
theorem real.sin_add_two_pi (x : ℝ) :
real.sin (x + 2 * real.pi) = real.sin x
source
@[simp]
theorem real.sin_sub_pi (x : ℝ) :
real.sin (x - real.pi) = -real.sin x
source
@[simp]
theorem real.sin_sub_two_pi (x : ℝ) :
real.sin (x - 2 * real.pi) = real.sin x
source
@[simp]
theorem real.sin_pi_sub (x : ℝ) :
real.sin (real.pi - x) = real.sin x
source
@[simp]
theorem real.sin_two_pi_sub (x : ℝ) :
real.sin (2 * real.pi - x) = -real.sin x
source
@[simp]
theorem real.sin_nat_mul_pi (n : ℕ) :
real.sin (↑n * real.pi) = 0
source
@[simp]
theorem real.sin_int_mul_pi (n : ℤ) :
real.sin (↑n * real.pi) = 0
source
@[simp]
theorem real.sin_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :
real.sin (x + ↑n * (2 * real.pi)) = real.sin x
source
@[simp]
theorem real.sin_add_int_mul_two_pi (x : ℝ) (n : ℤ) :
real.sin (x + ↑n * (2 * real.pi)) = real.sin x
source
@[simp]
theorem real.sin_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :
real.sin (x - ↑n * (2 * real.pi)) = real.sin x
source
@[simp]
theorem real.sin_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :
real.sin (x - ↑n * (2 * real.pi)) = real.sin x
source
@[simp]
theorem real.sin_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :
real.sin (↑n * (2 * real.pi) - x) = -real.sin x
source
@[simp]
theorem real.sin_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :
real.sin (↑n * (2 * real.pi) - x) = -real.sin x
source
theorem real.cos_antiperiodic  :
function.antiperiodic real.cos real.pi
source
theorem real.cos_periodic  :
function.periodic real.cos (2 * real.pi)
source
@[simp]
theorem real.cos_add_pi (x : ℝ) :
real.cos (x + real.pi) = -real.cos x
source
@[simp]
theorem real.cos_add_two_pi (x : ℝ) :
real.cos (x + 2 * real.pi) = real.cos x
source
@[simp]
theorem real.cos_sub_pi (x : ℝ) :
real.cos (x - real.pi) = -real.cos x
source
@[simp]
theorem real.cos_sub_two_pi (x : ℝ) :
real.cos (x - 2 * real.pi) = real.cos x
source
@[simp]
theorem real.cos_pi_sub (x : ℝ) :
real.cos (real.pi - x) = -real.cos x
source
@[simp]
theorem real.cos_two_pi_sub (x : ℝ) :
real.cos (2 * real.pi - x) = real.cos x
source
@[simp]
theorem real.cos_nat_mul_two_pi (n : ℕ) :
real.cos (↑n * (2 * real.pi)) = 1
source
@[simp]
theorem real.cos_int_mul_two_pi (n : ℤ) :
real.cos (↑n * (2 * real.pi)) = 1
source
@[simp]
theorem real.cos_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :
real.cos (x + ↑n * (2 * real.pi)) = real.cos x
source
@[simp]
theorem real.cos_add_int_mul_two_pi (x : ℝ) (n : ℤ) :
real.cos (x + ↑n * (2 * real.pi)) = real.cos x
source
@[simp]
theorem real.cos_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :
real.cos (x - ↑n * (2 * real.pi)) = real.cos x
source
@[simp]
theorem real.cos_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :
real.cos (x - ↑n * (2 * real.pi)) = real.cos x
source
@[simp]
theorem real.cos_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :
real.cos (↑n * (2 * real.pi) - x) = real.cos x
source
@[simp]
theorem real.cos_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :
real.cos (↑n * (2 * real.pi) - x) = real.cos x
source
@[simp]
theorem real.cos_nat_mul_two_pi_add_pi (n : ℕ) :
real.cos (↑n * (2 * real.pi) + real.pi) = -1
source
@[simp]
theorem real.cos_int_mul_two_pi_add_pi (n : ℤ) :
real.cos (↑n * (2 * real.pi) + real.pi) = -1
source
@[simp]
theorem real.cos_nat_mul_two_pi_sub_pi (n : ℕ) :
real.cos (↑n * (2 * real.pi) - real.pi) = -1
source
@[simp]
theorem real.cos_int_mul_two_pi_sub_pi (n : ℤ) :
real.cos (↑n * (2 * real.pi) - real.pi) = -1
source
theorem real.sin_pos_of_pos_of_lt_pi {x : ℝ} (h0x : 0 < x) (hxp : x < real.pi) :
0 < real.sin x
source
theorem real.sin_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ set.Ioo 0 real.pi) :
0 < real.sin x
source
theorem real.sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ set.Icc 0 real.pi) :
0 ≤ real.sin x
source
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ real.pi) :
0 ≤ real.sin x
source
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : ℝ} (hx0 : x < 0) (hpx : -real.pi < x) :
real.sin x < 0
source
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -real.pi ≤ x) :
real.sin x ≤ 0
source
@[simp]
theorem real.sin_pi_div_two  :
real.sin (real.pi / 2) = 1
source
theorem real.sin_add_pi_div_two (x : ℝ) :
real.sin (x + real.pi / 2) = real.cos x
source
theorem real.sin_sub_pi_div_two (x : ℝ) :
real.sin (x - real.pi / 2) = -real.cos x
source
theorem real.sin_pi_div_two_sub (x : ℝ) :
real.sin (real.pi / 2 - x) = real.cos x
source
theorem real.cos_add_pi_div_two (x : ℝ) :
real.cos (x + real.pi / 2) = -real.sin x
source
theorem real.cos_sub_pi_div_two (x : ℝ) :
real.cos (x - real.pi / 2) = real.sin x
source
theorem real.cos_pi_div_two_sub (x : ℝ) :
real.cos (real.pi / 2 - x) = real.sin x
source
theorem real.cos_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
0 < real.cos x
source
theorem real.cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :
0 ≤ real.cos x
source
theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : ℝ} (hl : -(real.pi / 2) ≤ x) (hu : x ≤ real.pi / 2) :
0 ≤ real.cos x
source
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : real.pi / 2 < x) (hx₂ : x < real.pi + real.pi / 2) :
real.cos x < 0
source
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} (hx₁ : real.pi / 2 ≤ x) (hx₂ : x ≤ real.pi + real.pi / 2) :
real.cos x ≤ 0
source
theorem real.sin_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ real.pi) :
real.sin x = real.sqrt (1 - real.cos x ^ 2)
source
theorem real.cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(real.pi / 2) ≤ x) (hu : x ≤ real.pi / 2) :
real.cos x = real.sqrt (1 - real.sin x ^ 2)
source
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -real.pi < x) (hx₂ : x < real.pi) :
real.sin x = 0 ↔ x = 0
source
theorem real.sin_eq_zero_iff {x : ℝ} :
real.sin x = 0 ↔ ∃ (n : ℤ), ↑n * real.pi = x
source
theorem real.sin_ne_zero_iff {x : ℝ} :
real.sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * real.pi ≠ x
source
theorem real.sin_eq_zero_iff_cos_eq {x : ℝ} :
real.sin x = 0 ↔ real.cos x = 1 ∨ real.cos x = -1
source
theorem real.cos_eq_one_iff (x : ℝ) :
real.cos x = 1 ↔ ∃ (n : ℤ), ↑n * (2 * real.pi) = x
source
theorem real.cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * real.pi) < x) (hx₂ : x < 2 * real.pi) :
real.cos x = 1 ↔ x = 0
source
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ real.pi / 2) (hxy : x < y) :
real.cos y < real.cos x
source
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ real.pi) (hxy : x < y) :
real.cos y < real.cos x
source
theorem real.strict_anti_on_cos  :
strict_anti_on real.cos (set.Icc 0 real.pi)
source
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ real.pi) (hxy : x ≤ y) :
real.cos y ≤ real.cos x
source
theorem real.sin_lt_sin_of_lt_of_le_pi_div_two {x y : ℝ} (hx₁ : -(real.pi / 2) ≤ x) (hy₂ : y ≤ real.pi / 2) (hxy : x < y) :
real.sin x < real.sin y
source
theorem real.strict_mono_on_sin  :
strict_mono_on real.sin (set.Icc (-(real.pi / 2)) (real.pi / 2))
source
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(real.pi / 2) ≤ x) (hy₂ : y ≤ real.pi / 2) (hxy : x ≤ y) :
real.sin x ≤ real.sin y
source
theorem real.inj_on_sin  :
set.inj_on real.sin (set.Icc (-(real.pi / 2)) (real.pi / 2))
source
theorem real.inj_on_cos  :
set.inj_on real.cos (set.Icc 0 real.pi)
source
theorem real.surj_on_sin  :
set.surj_on real.sin (set.Icc (-(real.pi / 2)) (real.pi / 2)) (set.Icc (-1) 1)
source
theorem real.surj_on_cos  :
set.surj_on real.cos (set.Icc 0 real.pi) (set.Icc (-1) 1)
source
theorem real.sin_mem_Icc (x : ℝ) :
real.sin x ∈ set.Icc (-1) 1
source
theorem real.cos_mem_Icc (x : ℝ) :
real.cos x ∈ set.Icc (-1) 1
source
theorem real.maps_to_sin (s : set ℝ) :
set.maps_to real.sin s (set.Icc (-1) 1)
source
theorem real.maps_to_cos (s : set ℝ) :
set.maps_to real.cos s (set.Icc (-1) 1)
source
theorem real.bij_on_sin  :
set.bij_on real.sin (set.Icc (-(real.pi / 2)) (real.pi / 2)) (set.Icc (-1) 1)
source
theorem real.bij_on_cos  :
set.bij_on real.cos (set.Icc 0 real.pi) (set.Icc (-1) 1)
source
@[simp]
theorem real.range_cos  :
set.range real.cos = set.Icc (-1) 1
source
@[simp]
theorem real.range_sin  :
set.range real.sin = set.Icc (-1) 1
source
theorem real.range_cos_infinite  :
(set.range real.cos).infinite
source
theorem real.range_sin_infinite  :
(set.range real.sin).infinite
source
@[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
source
theorem real.sqrt_two_add_series_zero (x : ℝ) :
real.sqrt_two_add_series x 0 = x
source
theorem real.sqrt_two_add_series_one  :
real.sqrt_two_add_series 0 1 = real.sqrt 2
source
theorem real.sqrt_two_add_series_two  :
real.sqrt_two_add_series 0 2 = real.sqrt (2 + real.sqrt 2)
source
theorem real.sqrt_two_add_series_zero_nonneg (n : ℕ) :
0 ≤ real.sqrt_two_add_series 0 n
source
theorem real.sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) (n : ℕ) :
0 ≤ real.sqrt_two_add_series x n
source
theorem real.sqrt_two_add_series_lt_two (n : ℕ) :
real.sqrt_two_add_series 0 n < 2
source
theorem real.sqrt_two_add_series_succ (x : ℝ) (n : ℕ) :
real.sqrt_two_add_series x (n + 1) = real.sqrt_two_add_series (real.sqrt (2 + x)) n
source
theorem real.sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) (n : ℕ) :
real.sqrt_two_add_series x n ≤ real.sqrt_two_add_series y n
source
@[simp]
theorem real.cos_pi_over_two_pow (n : ℕ) :
real.cos (real.pi / 2 ^ (n + 1)) = real.sqrt_two_add_series 0 n / 2
source
theorem real.sin_sq_pi_over_two_pow (n : ℕ) :
real.sin (real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (real.sqrt_two_add_series 0 n / 2) ^ 2
source
theorem real.sin_sq_pi_over_two_pow_succ (n : ℕ) :
real.sin (real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - real.sqrt_two_add_series 0 n / 4
source
@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ℕ) :
real.sin (real.pi / 2 ^ (n + 2)) = real.sqrt (2 - real.sqrt_two_add_series 0 n) / 2
source
@[simp]
theorem real.cos_pi_div_four  :
real.cos (real.pi / 4) = real.sqrt 2 / 2
source
@[simp]
theorem real.sin_pi_div_four  :
real.sin (real.pi / 4) = real.sqrt 2 / 2
source
@[simp]
theorem real.cos_pi_div_eight  :
real.cos (real.pi / 8) = real.sqrt (2 + real.sqrt 2) / 2
source
@[simp]
theorem real.sin_pi_div_eight  :
real.sin (real.pi / 8) = real.sqrt (2 - real.sqrt 2) / 2
source
@[simp]
theorem real.cos_pi_div_sixteen  :
real.cos (real.pi / 16) = real.sqrt (2 + real.sqrt (2 + real.sqrt 2)) / 2
source
@[simp]
theorem real.sin_pi_div_sixteen  :
real.sin (real.pi / 16) = real.sqrt (2 - real.sqrt (2 + real.sqrt 2)) / 2
source
@[simp]
theorem real.cos_pi_div_thirty_two  :
real.cos (real.pi / 32) = real.sqrt (2 + real.sqrt (2 + real.sqrt (2 + real.sqrt 2))) / 2
source
@[simp]
theorem real.sin_pi_div_thirty_two  :
real.sin (real.pi / 32) = real.sqrt (2 - real.sqrt (2 + real.sqrt (2 + real.sqrt 2))) / 2
source
@[simp]
theorem real.cos_pi_div_three  :
real.cos (real.pi / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

source
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).

source
@[simp]
theorem real.cos_pi_div_six  :
real.cos (real.pi / 6) = real.sqrt 3 / 2

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

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

The sine of π / 6 is 1 / 2.

source
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).

source
@[simp]
theorem real.sin_pi_div_three  :
real.sin (real.pi / 3) = real.sqrt 3 / 2

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

source
noncomputable def real.sin_order_iso  :
↥(set.Icc (-(real.pi / 2)) (real.pi / 2)) ≃o ↥(set.Icc (-1) 1)

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

Equations
source
@[simp]
theorem real.coe_sin_order_iso_apply (x : ↥(set.Icc (-(real.pi / 2)) (real.pi / 2))) :
↑(⇑real.sin_order_iso x) = real.sin ↑x
source
theorem real.sin_order_iso_apply (x : ↥(set.Icc (-(real.pi / 2)) (real.pi / 2))) :
⇑real.sin_order_iso x = ⟨real.sin ↑x, _⟩
source
@[simp]
theorem real.tan_pi_div_four  :
real.tan (real.pi / 4) = 1
source
@[simp]
theorem real.tan_pi_div_two  :
real.tan (real.pi / 2) = 0
source
theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < real.pi / 2) :
0 < real.tan x
source
theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ real.pi / 2) :
0 ≤ real.tan x
source
theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(real.pi / 2) < x) :
real.tan x < 0
source
theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -(real.pi / 2) ≤ x) :
real.tan x ≤ 0
source
theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y < real.pi / 2) (hxy : x < y) :
real.tan x < real.tan y
source
theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(real.pi / 2) < x) (hy₂ : y < real.pi / 2) (hxy : x < y) :
real.tan x < real.tan y
source
theorem real.strict_mono_on_tan  :
strict_mono_on real.tan (set.Ioo (-(real.pi / 2)) (real.pi / 2))
source
theorem real.inj_on_tan  :
set.inj_on real.tan (set.Ioo (-(real.pi / 2)) (real.pi / 2))
source
theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(real.pi / 2) < x) (hx₂ : x < real.pi / 2) (hy₁ : -(real.pi / 2) < y) (hy₂ : y < real.pi / 2) (hxy : real.tan x = real.tan y) :
x = y
source
theorem real.tan_periodic  :
function.periodic real.tan real.pi
source
theorem real.tan_add_pi (x : ℝ) :
real.tan (x + real.pi) = real.tan x
source
theorem real.tan_sub_pi (x : ℝ) :
real.tan (x - real.pi) = real.tan x
source
theorem real.tan_pi_sub (x : ℝ) :
real.tan (real.pi - x) = -real.tan x
source
theorem real.tan_pi_div_two_sub (x : ℝ) :
real.tan (real.pi / 2 - x) = (real.tan x)⁻¹
source
theorem real.tan_nat_mul_pi (n : ℕ) :
real.tan (↑n * real.pi) = 0
source
theorem real.tan_int_mul_pi (n : ℤ) :
real.tan (↑n * real.pi) = 0
source
theorem real.tan_add_nat_mul_pi (x : ℝ) (n : ℕ) :
real.tan (x + ↑n * real.pi) = real.tan x
source
theorem real.tan_add_int_mul_pi (x : ℝ) (n : ℤ) :
real.tan (x + ↑n * real.pi) = real.tan x
source
theorem real.tan_sub_nat_mul_pi (x : ℝ) (n : ℕ) :
real.tan (x - ↑n * real.pi) = real.tan x
source
theorem real.tan_sub_int_mul_pi (x : ℝ) (n : ℤ) :
real.tan (x - ↑n * real.pi) = real.tan x
source
theorem real.tan_nat_mul_pi_sub (x : ℝ) (n : ℕ) :
real.tan (↑n * real.pi - x) = -real.tan x
source
theorem real.tan_int_mul_pi_sub (x : ℝ) (n : ℤ) :
real.tan (↑n * real.pi - x) = -real.tan x
source
theorem real.tendsto_sin_pi_div_two  :
filter.tendsto real.sin (nhds_within (real.pi / 2) (set.Iio (real.pi / 2))) (nhds 1)
source
theorem real.tendsto_cos_pi_div_two  :
filter.tendsto real.cos (nhds_within (real.pi / 2) (set.Iio (real.pi / 2))) (nhds_within 0 (set.Ioi 0))
source
theorem real.tendsto_tan_pi_div_two  :
filter.tendsto real.tan (nhds_within (real.pi / 2) (set.Iio (real.pi / 2))) filter.at_top
source
theorem real.tendsto_sin_neg_pi_div_two  :
filter.tendsto real.sin (nhds_within (-(real.pi / 2)) (set.Ioi (-(real.pi / 2)))) (nhds (-1))
source
theorem real.tendsto_cos_neg_pi_div_two  :
filter.tendsto real.cos (nhds_within (-(real.pi / 2)) (set.Ioi (-(real.pi / 2)))) (nhds_within 0 (set.Ioi 0))
source
theorem real.tendsto_tan_neg_pi_div_two  :
filter.tendsto real.tan (nhds_within (-(real.pi / 2)) (set.Ioi (-(real.pi / 2)))) filter.at_bot
source
theorem complex.sin_eq_zero_iff_cos_eq {z : ℂ} :
complex.sin z = 0 ↔ complex.cos z = 1 ∨ complex.cos z = -1
source
@[simp]
theorem complex.cos_pi_div_two  :
complex.cos (↑real.pi / 2) = 0
source
@[simp]
theorem complex.sin_pi_div_two  :
complex.sin (↑real.pi / 2) = 1
source
@[simp]
theorem complex.sin_pi  :
complex.sin ↑real.pi = 0
source
@[simp]
theorem complex.cos_pi  :
complex.cos ↑real.pi = -1
source
@[simp]
theorem complex.sin_two_pi  :
complex.sin (2 * ↑real.pi) = 0
source
@[simp]
theorem complex.cos_two_pi  :
complex.cos (2 * ↑real.pi) = 1
source
theorem complex.sin_antiperiodic  :
function.antiperiodic complex.sin ↑real.pi
source
theorem complex.sin_periodic  :
function.periodic complex.sin (2 * ↑real.pi)
source
theorem complex.sin_add_pi (x : ℂ) :
complex.sin (x + ↑real.pi) = -complex.sin x
source
theorem complex.sin_add_two_pi (x : ℂ) :
complex.sin (x + 2 * ↑real.pi) = complex.sin x
source
theorem complex.sin_sub_pi (x : ℂ) :
complex.sin (x - ↑real.pi) = -complex.sin x
source
theorem complex.sin_sub_two_pi (x : ℂ) :
complex.sin (x - 2 * ↑real.pi) = complex.sin x
source
theorem complex.sin_pi_sub (x : ℂ) :
complex.sin (↑real.pi - x) = complex.sin x
source
theorem complex.sin_two_pi_sub (x : ℂ) :
complex.sin (2 * ↑real.pi - x) = -complex.sin x
source
theorem complex.sin_nat_mul_pi (n : ℕ) :
complex.sin (↑n * ↑real.pi) = 0
source
theorem complex.sin_int_mul_pi (n : ℤ) :
complex.sin (↑n * ↑real.pi) = 0
source
theorem complex.sin_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :
complex.sin (x + ↑n * (2 * ↑real.pi)) = complex.sin x
source
theorem complex.sin_add_int_mul_two_pi (x : ℂ) (n : ℤ) :
complex.sin (x + ↑n * (2 * ↑real.pi)) = complex.sin x
source
theorem complex.sin_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :
complex.sin (x - ↑n * (2 * ↑real.pi)) = complex.sin x
source
theorem complex.sin_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :
complex.sin (x - ↑n * (2 * ↑real.pi)) = complex.sin x
source
theorem complex.sin_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :
complex.sin (↑n * (2 * ↑real.pi) - x) = -complex.sin x
source
theorem complex.sin_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :
complex.sin (↑n * (2 * ↑real.pi) - x) = -complex.sin x
source
theorem complex.cos_antiperiodic  :
function.antiperiodic complex.cos ↑real.pi
source
theorem complex.cos_periodic  :
function.periodic complex.cos (2 * ↑real.pi)
source
theorem complex.cos_add_pi (x : ℂ) :
complex.cos (x + ↑real.pi) = -complex.cos x
source
theorem complex.cos_add_two_pi (x : ℂ) :
complex.cos (x + 2 * ↑real.pi) = complex.cos x
source
theorem complex.cos_sub_pi (x : ℂ) :
complex.cos (x - ↑real.pi) = -complex.cos x
source
theorem complex.cos_sub_two_pi (x : ℂ) :
complex.cos (x - 2 * ↑real.pi) = complex.cos x
source
theorem complex.cos_pi_sub (x : ℂ) :
complex.cos (↑real.pi - x) = -complex.cos x
source
theorem complex.cos_two_pi_sub (x : ℂ) :
complex.cos (2 * ↑real.pi - x) = complex.cos x
source
theorem complex.cos_nat_mul_two_pi (n : ℕ) :
complex.cos (↑n * (2 * ↑real.pi)) = 1
source
theorem complex.cos_int_mul_two_pi (n : ℤ) :
complex.cos (↑n * (2 * ↑real.pi)) = 1
source
theorem complex.cos_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :
complex.cos (x + ↑n * (2 * ↑real.pi)) = complex.cos x
source
theorem complex.cos_add_int_mul_two_pi (x : ℂ) (n : ℤ) :
complex.cos (x + ↑n * (2 * ↑real.pi)) = complex.cos x
source
theorem complex.cos_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :
complex.cos (x - ↑n * (2 * ↑real.pi)) = complex.cos x
source
theorem complex.cos_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :
complex.cos (x - ↑n * (2 * ↑real.pi)) = complex.cos x
source
theorem complex.cos_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :
complex.cos (↑n * (2 * ↑real.pi) - x) = complex.cos x
source
theorem complex.cos_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :
complex.cos (↑n * (2 * ↑real.pi) - x) = complex.cos x
source
theorem complex.cos_nat_mul_two_pi_add_pi (n : ℕ) :
complex.cos (↑n * (2 * ↑real.pi) + ↑real.pi) = -1
source
theorem complex.cos_int_mul_two_pi_add_pi (n : ℤ) :
complex.cos (↑n * (2 * ↑real.pi) + ↑real.pi) = -1
source
theorem complex.cos_nat_mul_two_pi_sub_pi (n : ℕ) :
complex.cos (↑n * (2 * ↑real.pi) - ↑real.pi) = -1
source
theorem complex.cos_int_mul_two_pi_sub_pi (n : ℤ) :
complex.cos (↑n * (2 * ↑real.pi) - ↑real.pi) = -1
source
theorem complex.sin_add_pi_div_two (x : ℂ) :
complex.sin (x + ↑real.pi / 2) = complex.cos x
source
theorem complex.sin_sub_pi_div_two (x : ℂ) :
complex.sin (x - ↑real.pi / 2) = -complex.cos x
source
theorem complex.sin_pi_div_two_sub (x : ℂ) :
complex.sin (↑real.pi / 2 - x) = complex.cos x
source
theorem complex.cos_add_pi_div_two (x : ℂ) :
complex.cos (x + ↑real.pi / 2) = -complex.sin x
source
theorem complex.cos_sub_pi_div_two (x : ℂ) :
complex.cos (x - ↑real.pi / 2) = complex.sin x
source
theorem complex.cos_pi_div_two_sub (x : ℂ) :
complex.cos (↑real.pi / 2 - x) = complex.sin x
source
theorem complex.tan_periodic  :
function.periodic complex.tan ↑real.pi
source
theorem complex.tan_add_pi (x : ℂ) :
complex.tan (x + ↑real.pi) = complex.tan x
source
theorem complex.tan_sub_pi (x : ℂ) :
complex.tan (x - ↑real.pi) = complex.tan x
source
theorem complex.tan_pi_sub (x : ℂ) :
complex.tan (↑real.pi - x) = -complex.tan x
source
theorem complex.tan_pi_div_two_sub (x : ℂ) :
complex.tan (↑real.pi / 2 - x) = (complex.tan x)⁻¹
source
theorem complex.tan_nat_mul_pi (n : ℕ) :
complex.tan (↑n * ↑real.pi) = 0
source
theorem complex.tan_int_mul_pi (n : ℤ) :
complex.tan (↑n * ↑real.pi) = 0
source
theorem complex.tan_add_nat_mul_pi (x : ℂ) (n : ℕ) :
complex.tan (x + ↑n * ↑real.pi) = complex.tan x
source
theorem complex.tan_add_int_mul_pi (x : ℂ) (n : ℤ) :
complex.tan (x + ↑n * ↑real.pi) = complex.tan x
source
theorem complex.tan_sub_nat_mul_pi (x : ℂ) (n : ℕ) :
complex.tan (x - ↑n * ↑real.pi) = complex.tan x
source
theorem complex.tan_sub_int_mul_pi (x : ℂ) (n : ℤ) :
complex.tan (x - ↑n * ↑real.pi) = complex.tan x
source
theorem complex.tan_nat_mul_pi_sub (x : ℂ) (n : ℕ) :
complex.tan (↑n * ↑real.pi - x) = -complex.tan x
source
theorem complex.tan_int_mul_pi_sub (x : ℂ) (n : ℤ) :
complex.tan (↑n * ↑real.pi - x) = -complex.tan x
source
theorem complex.exp_antiperiodic  :
function.antiperiodic complex.exp (↑real.pi * complex.I)
source
theorem complex.exp_periodic  :
function.periodic complex.exp (2 * ↑real.pi * complex.I)
source
theorem complex.exp_mul_I_antiperiodic  :
function.antiperiodic (λ (x : ℂ), complex.exp (x * complex.I)) ↑real.pi
source
theorem complex.exp_mul_I_periodic  :
function.periodic (λ (x : ℂ), complex.exp (x * complex.I)) (2 * ↑real.pi)
source
@[simp]
theorem complex.exp_pi_mul_I  :
complex.exp (↑real.pi * complex.I) = -1
source
@[simp]
theorem complex.exp_two_pi_mul_I  :
complex.exp (2 * ↑real.pi * complex.I) = 1
source
@[simp]
theorem complex.exp_nat_mul_two_pi_mul_I (n : ℕ) :
complex.exp (↑n * (2 * ↑real.pi * complex.I)) = 1
source
@[simp]
theorem complex.exp_int_mul_two_pi_mul_I (n : ℤ) :
complex.exp (↑n * (2 * ↑real.pi * complex.I)) = 1
source
@[simp]
theorem complex.exp_add_pi_mul_I (z : ℂ) :
complex.exp (z + ↑real.pi * complex.I) = -complex.exp z
source
@[simp]
theorem complex.exp_sub_pi_mul_I (z : ℂ) :
complex.exp (z - ↑real.pi * complex.I) = -complex.exp z
source
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 ≤ real.pi / 2) :
⇑complex.abs (complex.exp (↑a * (complex.exp z + complex.exp (-z)))) ≤ real.exp (a * real.cos b * real.exp |z.re|)

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|}}.$$