Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Trigonometric functions #

Main definitions #

This file contains the definition of π.

See also Analysis.SpecialFunctions.Trigonometric.Inverse and Analysis.SpecialFunctions.Trigonometric.Arctan for the inverse trigonometric functions.

See also Analysis.SpecialFunctions.Complex.Arg and Analysis.SpecialFunctions.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.SpecialFunctions.Trigonometric.Complex, as they are most easily proved by appealing to the corresponding fact for complex trigonometric functions.

See also Analysis.SpecialFunctions.Trigonometric.Chebyshev for the multiple angle formulas in terms of Chebyshev polynomials.

Tags #

sin, cos, tan, angle

theorem Complex.continuous_sin :

Continuous Complex.sin

theorem Complex.continuousOn_sin {s : Set ℂ} :

ContinuousOn Complex.sin s

theorem Complex.continuous_cos :

Continuous Complex.cos

theorem Complex.continuousOn_cos {s : Set ℂ} :

ContinuousOn Complex.cos s

theorem Complex.continuous_sinh :

Continuous Complex.sinh

theorem Complex.continuous_cosh :

Continuous Complex.cosh

theorem Real.continuous_sin :

Continuous Real.sin

theorem Real.continuousOn_sin {s : Set ℝ} :

ContinuousOn Real.sin s

theorem Real.continuous_cos :

Continuous Real.cos

theorem Real.continuousOn_cos {s : Set ℝ} :

ContinuousOn Real.cos s

theorem Real.continuous_sinh :

Continuous Real.sinh

theorem Real.continuous_cosh :

Continuous Real.cosh

theorem Real.exists_cos_eq_zero :

0 ∈ Real.cos '' Set.Icc 1 2

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

Real.pi = 2 * Classical.choose Real.exists_cos_eq_zero

Instances For

def Real.termπ :

Lean.ParserDescr

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

Real.termπ = Lean.ParserDescr.node `Real.termπ 1024 (Lean.ParserDescr.symbol "π")

Instances For

@[simp]

theorem Real.cos_pi_div_two :

Real.cos (Real.pi / 2) = 0

theorem Real.one_le_pi_div_two :

1 ≤ Real.pi / 2

theorem Real.pi_div_two_le_two :

Real.pi / 2 ≤ 2

theorem Real.two_le_pi :

theorem Real.pi_le_four :

theorem Real.pi_pos :

theorem Real.pi_nonneg :

theorem Real.pi_ne_zero :

theorem Real.pi_div_two_pos :

0 < Real.pi / 2

theorem Real.two_pi_pos :

0 < 2 * Real.pi

def Mathlib.Meta.Positivity.evalRealPi :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: π is always positive.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NNReal.pi :

π considered as a nonnegative real.

Equations

NNReal.pi = { val := Real.pi, property := NNReal.pi.proof_1 }

Instances For

@[simp]

theorem NNReal.coe_real_pi :

↑NNReal.pi = Real.pi

theorem NNReal.pi_pos :

theorem NNReal.pi_ne_zero :

NNReal.pi ≠ 0

@[simp]

theorem Real.sin_pi :

Real.sin Real.pi = 0

@[simp]

theorem Real.cos_pi :

Real.cos Real.pi = -1

@[simp]

theorem Real.sin_two_pi :

Real.sin (2 * Real.pi) = 0

@[simp]

theorem Real.cos_two_pi :

Real.cos (2 * Real.pi) = 1

theorem Real.sin_antiperiodic :

Function.Antiperiodic Real.sin Real.pi

theorem Real.sin_periodic :

Function.Periodic Real.sin (2 * Real.pi)

@[simp]

theorem Real.sin_add_pi (x : ℝ) :

Real.sin (x + Real.pi) = -Real.sin x

@[simp]

theorem Real.sin_add_two_pi (x : ℝ) :

Real.sin (x + 2 * Real.pi) = Real.sin x

@[simp]

theorem Real.sin_sub_pi (x : ℝ) :

Real.sin (x - Real.pi) = -Real.sin x

@[simp]

theorem Real.sin_sub_two_pi (x : ℝ) :

Real.sin (x - 2 * Real.pi) = Real.sin x

@[simp]

theorem Real.sin_pi_sub (x : ℝ) :

Real.sin (Real.pi - x) = Real.sin x

@[simp]

theorem Real.sin_two_pi_sub (x : ℝ) :

Real.sin (2 * Real.pi - x) = -Real.sin x

@[simp]

theorem Real.sin_nat_mul_pi (n : ℕ) :

Real.sin (↑n * Real.pi) = 0

@[simp]

theorem Real.sin_int_mul_pi (n : ℤ) :

Real.sin (↑n * Real.pi) = 0

@[simp]

theorem Real.sin_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :

Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x

@[simp]

theorem Real.sin_add_int_mul_two_pi (x : ℝ) (n : ℤ) :

Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x

@[simp]

theorem Real.sin_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :

Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x

@[simp]

theorem Real.sin_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :

Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x

@[simp]

theorem Real.sin_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :

Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x

@[simp]

theorem Real.sin_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :

Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x

theorem Real.cos_antiperiodic :

Function.Antiperiodic Real.cos Real.pi

theorem Real.cos_periodic :

Function.Periodic Real.cos (2 * Real.pi)

@[simp]

theorem Real.cos_add_pi (x : ℝ) :

Real.cos (x + Real.pi) = -Real.cos x

@[simp]

theorem Real.cos_add_two_pi (x : ℝ) :

Real.cos (x + 2 * Real.pi) = Real.cos x

@[simp]

theorem Real.cos_sub_pi (x : ℝ) :

Real.cos (x - Real.pi) = -Real.cos x

@[simp]

theorem Real.cos_sub_two_pi (x : ℝ) :

Real.cos (x - 2 * Real.pi) = Real.cos x

@[simp]

theorem Real.cos_pi_sub (x : ℝ) :

Real.cos (Real.pi - x) = -Real.cos x

@[simp]

theorem Real.cos_two_pi_sub (x : ℝ) :

Real.cos (2 * Real.pi - x) = Real.cos 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)) = Real.cos x

@[simp]

theorem Real.cos_add_int_mul_two_pi (x : ℝ) (n : ℤ) :

Real.cos (x + ↑n * (2 * Real.pi)) = Real.cos x

@[simp]

theorem Real.cos_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :

Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x

@[simp]

theorem Real.cos_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :

Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x

@[simp]

theorem Real.cos_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :

Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x

@[simp]

theorem Real.cos_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :

Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x

theorem Real.cos_nat_mul_two_pi_add_pi (n : ℕ) :

Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1

theorem Real.cos_int_mul_two_pi_add_pi (n : ℤ) :

Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1

theorem Real.cos_nat_mul_two_pi_sub_pi (n : ℕ) :

Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1

theorem Real.cos_int_mul_two_pi_sub_pi (n : ℤ) :

Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1

theorem Real.sin_pos_of_pos_of_lt_pi {x : ℝ} (h0x : 0 < x) (hxp : x < Real.pi) :

theorem Real.sin_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo 0 Real.pi) :

theorem Real.sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Set.Icc 0 Real.pi) :

0 ≤ Real.sin x

theorem Real.sin_nonneg_of_nonneg_of_le_pi {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ Real.pi) :

0 ≤ Real.sin x

theorem Real.sin_neg_of_neg_of_neg_pi_lt {x : ℝ} (hx0 : x < 0) (hpx : -Real.pi < x) :

theorem Real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -Real.pi ≤ x) :

Real.sin x ≤ 0

@[simp]

theorem Real.sin_pi_div_two :

Real.sin (Real.pi / 2) = 1

theorem Real.sin_add_pi_div_two (x : ℝ) :

Real.sin (x + Real.pi / 2) = Real.cos x

theorem Real.sin_sub_pi_div_two (x : ℝ) :

Real.sin (x - Real.pi / 2) = -Real.cos x

theorem Real.sin_pi_div_two_sub (x : ℝ) :

Real.sin (Real.pi / 2 - x) = Real.cos x

theorem Real.cos_add_pi_div_two (x : ℝ) :

Real.cos (x + Real.pi / 2) = -Real.sin x

theorem Real.cos_sub_pi_div_two (x : ℝ) :

Real.cos (x - Real.pi / 2) = Real.sin x

theorem Real.cos_pi_div_two_sub (x : ℝ) :

Real.cos (Real.pi / 2 - x) = Real.sin x

theorem Real.cos_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :

theorem Real.cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :

0 ≤ Real.cos x

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

theorem Real.cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : Real.pi / 2 < x) (hx₂ : x < Real.pi + Real.pi / 2) :

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

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)

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)

theorem Real.cos_half {x : ℝ} (hl : -Real.pi ≤ x) (hr : x ≤ Real.pi) :

Real.cos (x / 2) = Real.sqrt ((1 + Real.cos x) / 2)

theorem Real.abs_sin_half (x : ℝ) :

|Real.sin (x / 2)| = Real.sqrt ((1 - Real.cos x) / 2)

theorem Real.sin_half_eq_sqrt {x : ℝ} (hl : 0 ≤ x) (hr : x ≤ 2 * Real.pi) :

Real.sin (x / 2) = Real.sqrt ((1 - Real.cos x) / 2)

theorem Real.sin_half_eq_neg_sqrt {x : ℝ} (hl : -(2 * Real.pi) ≤ x) (hr : x ≤ 0) :

Real.sin (x / 2) = -Real.sqrt ((1 - Real.cos x) / 2)

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

theorem Real.sin_eq_zero_iff {x : ℝ} :

Real.sin x = 0 ↔ ∃ (n : ℤ), ↑n * Real.pi = x

theorem Real.sin_ne_zero_iff {x : ℝ} :

Real.sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * Real.pi ≠ x

theorem Real.sin_eq_zero_iff_cos_eq {x : ℝ} :

Real.sin x = 0 ↔ Real.cos x = 1 ∨ Real.cos x = -1

theorem Real.cos_eq_one_iff (x : ℝ) :

Real.cos 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 < 2 * Real.pi) :

Real.cos x = 1 ↔ x = 0

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

theorem Real.strictMonoOn_sin :

StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))

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

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

theorem Real.strictAntiOn_cos :

StrictAntiOn Real.cos (Set.Icc 0 Real.pi)

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

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

theorem Real.injOn_sin :

Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))

theorem Real.injOn_cos :

Set.InjOn Real.cos (Set.Icc 0 Real.pi)

theorem Real.surjOn_sin :

Set.SurjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)

theorem Real.surjOn_cos :

Set.SurjOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)

theorem Real.sin_mem_Icc (x : ℝ) :

Real.sin x ∈ Set.Icc (-1) 1

theorem Real.cos_mem_Icc (x : ℝ) :

Real.cos x ∈ Set.Icc (-1) 1

theorem Real.mapsTo_sin (s : Set ℝ) :

Set.MapsTo Real.sin s (Set.Icc (-1) 1)

theorem Real.mapsTo_cos (s : Set ℝ) :

Set.MapsTo Real.cos s (Set.Icc (-1) 1)

theorem Real.bijOn_sin :

Set.BijOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)

theorem Real.bijOn_cos :

Set.BijOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)

@[simp]

theorem Real.range_cos :

Set.range Real.cos = Set.Icc (-1) 1

@[simp]

theorem Real.range_sin :

Set.range Real.sin = Set.Icc (-1) 1

theorem Real.range_cos_infinite :

Set.Infinite (Set.range Real.cos)

theorem Real.range_sin_infinite :

Set.Infinite (Set.range Real.sin)

noncomputable def Real.sqrtTwoAddSeries (x : ℝ) :

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

Equations

Real.sqrtTwoAddSeries x 0 = x
Real.sqrtTwoAddSeries x (Nat.succ n) = Real.sqrt (2 + Real.sqrtTwoAddSeries x n)

Instances For

theorem Real.sqrtTwoAddSeries_zero (x : ℝ) :

Real.sqrtTwoAddSeries x 0 = x

theorem Real.sqrtTwoAddSeries_one :

Real.sqrtTwoAddSeries 0 1 = Real.sqrt 2

theorem Real.sqrtTwoAddSeries_two :

Real.sqrtTwoAddSeries 0 2 = Real.sqrt (2 + Real.sqrt 2)

theorem Real.sqrtTwoAddSeries_zero_nonneg (n : ℕ) :

0 ≤ Real.sqrtTwoAddSeries 0 n

theorem Real.sqrtTwoAddSeries_nonneg {x : ℝ} (h : 0 ≤ x) (n : ℕ) :

0 ≤ Real.sqrtTwoAddSeries x n

theorem Real.sqrtTwoAddSeries_lt_two (n : ℕ) :

Real.sqrtTwoAddSeries 0 n < 2

theorem Real.sqrtTwoAddSeries_succ (x : ℝ) (n : ℕ) :

Real.sqrtTwoAddSeries x (n + 1) = Real.sqrtTwoAddSeries (Real.sqrt (2 + x)) n

theorem Real.sqrtTwoAddSeries_monotone_left {x : ℝ} {y : ℝ} (h : x ≤ y) (n : ℕ) :

Real.sqrtTwoAddSeries x n ≤ Real.sqrtTwoAddSeries y n

@[simp]

theorem Real.cos_pi_over_two_pow (n : ℕ) :

Real.cos (Real.pi / 2 ^ (n + 1)) = Real.sqrtTwoAddSeries 0 n / 2

theorem Real.sin_sq_pi_over_two_pow (n : ℕ) :

Real.sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2

theorem Real.sin_sq_pi_over_two_pow_succ (n : ℕ) :

Real.sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - Real.sqrtTwoAddSeries 0 n / 4

@[simp]

theorem Real.sin_pi_over_two_pow_succ (n : ℕ) :

Real.sin (Real.pi / 2 ^ (n + 2)) = Real.sqrt (2 - Real.sqrtTwoAddSeries 0 n) / 2

@[simp]

theorem Real.cos_pi_div_four :

Real.cos (Real.pi / 4) = Real.sqrt 2 / 2

@[simp]

theorem Real.sin_pi_div_four :

Real.sin (Real.pi / 4) = Real.sqrt 2 / 2

@[simp]

theorem Real.cos_pi_div_eight :

Real.cos (Real.pi / 8) = Real.sqrt (2 + Real.sqrt 2) / 2

@[simp]

theorem Real.sin_pi_div_eight :

Real.sin (Real.pi / 8) = Real.sqrt (2 - Real.sqrt 2) / 2

@[simp]

theorem Real.cos_pi_div_sixteen :

Real.cos (Real.pi / 16) = Real.sqrt (2 + Real.sqrt (2 + Real.sqrt 2)) / 2

@[simp]

theorem Real.sin_pi_div_sixteen :

Real.sin (Real.pi / 16) = Real.sqrt (2 - Real.sqrt (2 + Real.sqrt 2)) / 2

@[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

@[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

@[simp]

theorem Real.cos_pi_div_three :

Real.cos (Real.pi / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

@[simp]

theorem Real.cos_pi_div_six :

Real.cos (Real.pi / 6) = Real.sqrt 3 / 2

The cosine of π / 6 is √3 / 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.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 :

Real.sin (Real.pi / 3) = Real.sqrt 3 / 2

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

def Real.sinOrderIso :

↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) ≃o ↑(Set.Icc (-1) 1)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Real.coe_sinOrderIso_apply (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :

↑(Real.sinOrderIso x) = Real.sin ↑x

theorem Real.sinOrderIso_apply (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :

Real.sinOrderIso x = { val := Real.sin ↑x, property := ⋯ }

@[simp]

theorem Real.tan_pi_div_four :

Real.tan (Real.pi / 4) = 1

@[simp]

theorem Real.tan_pi_div_two :

Real.tan (Real.pi / 2) = 0

@[simp]

theorem Real.tan_pi_div_six :

Real.tan (Real.pi / 6) = 1 / Real.sqrt 3

@[simp]

theorem Real.tan_pi_div_three :

Real.tan (Real.pi / 3) = Real.sqrt 3

theorem Real.tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < Real.pi / 2) :

theorem Real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ Real.pi / 2) :

0 ≤ Real.tan x

theorem Real.tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(Real.pi / 2) < x) :

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

theorem Real.strictMonoOn_tan :

StrictMonoOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))

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

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

theorem Real.injOn_tan :

Set.InjOn Real.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 < Real.pi / 2) (hy₁ : -(Real.pi / 2) < y) (hy₂ : y < Real.pi / 2) (hxy : Real.tan x = Real.tan y) :

x = y

theorem Real.tan_periodic :

Function.Periodic Real.tan Real.pi

@[simp]

theorem Real.tan_pi :

Real.tan Real.pi = 0

theorem Real.tan_add_pi (x : ℝ) :

Real.tan (x + Real.pi) = Real.tan x

theorem Real.tan_sub_pi (x : ℝ) :

Real.tan (x - Real.pi) = Real.tan x

theorem Real.tan_pi_sub (x : ℝ) :

Real.tan (Real.pi - x) = -Real.tan x

theorem Real.tan_pi_div_two_sub (x : ℝ) :

Real.tan (Real.pi / 2 - x) = (Real.tan x)⁻¹

theorem Real.tan_nat_mul_pi (n : ℕ) :

Real.tan (↑n * Real.pi) = 0

theorem Real.tan_int_mul_pi (n : ℤ) :

Real.tan (↑n * Real.pi) = 0

theorem Real.tan_add_nat_mul_pi (x : ℝ) (n : ℕ) :

Real.tan (x + ↑n * Real.pi) = Real.tan x

theorem Real.tan_add_int_mul_pi (x : ℝ) (n : ℤ) :

Real.tan (x + ↑n * Real.pi) = Real.tan x

theorem Real.tan_sub_nat_mul_pi (x : ℝ) (n : ℕ) :

Real.tan (x - ↑n * Real.pi) = Real.tan x

theorem Real.tan_sub_int_mul_pi (x : ℝ) (n : ℤ) :

Real.tan (x - ↑n * Real.pi) = Real.tan x

theorem Real.tan_nat_mul_pi_sub (x : ℝ) (n : ℕ) :

Real.tan (↑n * Real.pi - x) = -Real.tan x

theorem Real.tan_int_mul_pi_sub (x : ℝ) (n : ℤ) :

Real.tan (↑n * Real.pi - x) = -Real.tan x

theorem Real.tendsto_sin_pi_div_two :

Filter.Tendsto Real.sin (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhds 1)

theorem Real.tendsto_cos_pi_div_two :

Filter.Tendsto Real.cos (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhdsWithin 0 (Set.Ioi 0))

theorem Real.tendsto_tan_pi_div_two :

Filter.Tendsto Real.tan (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) Filter.atTop

theorem Real.tendsto_sin_neg_pi_div_two :

Filter.Tendsto Real.sin (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhds (-1))

theorem Real.tendsto_cos_neg_pi_div_two :

Filter.Tendsto Real.cos (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhdsWithin 0 (Set.Ioi 0))

theorem Real.tendsto_tan_neg_pi_div_two :

Filter.Tendsto Real.tan (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) Filter.atBot

theorem Complex.sin_eq_zero_iff_cos_eq {z : ℂ} :

Complex.sin z = 0 ↔ Complex.cos z = 1 ∨ Complex.cos z = -1

@[simp]

theorem Complex.cos_pi_div_two :

Complex.cos (↑Real.pi / 2) = 0

@[simp]

theorem Complex.sin_pi_div_two :

Complex.sin (↑Real.pi / 2) = 1

@[simp]

theorem Complex.sin_pi :

Complex.sin ↑Real.pi = 0

@[simp]

theorem Complex.cos_pi :

Complex.cos ↑Real.pi = -1

@[simp]

theorem Complex.sin_two_pi :

Complex.sin (2 * ↑Real.pi) = 0

@[simp]

theorem Complex.cos_two_pi :

Complex.cos (2 * ↑Real.pi) = 1

theorem Complex.sin_antiperiodic :

Function.Antiperiodic Complex.sin ↑Real.pi

theorem Complex.sin_periodic :

Function.Periodic Complex.sin (2 * ↑Real.pi)

theorem Complex.sin_add_pi (x : ℂ) :

Complex.sin (x + ↑Real.pi) = -Complex.sin x

theorem Complex.sin_add_two_pi (x : ℂ) :

Complex.sin (x + 2 * ↑Real.pi) = Complex.sin x

theorem Complex.sin_sub_pi (x : ℂ) :

Complex.sin (x - ↑Real.pi) = -Complex.sin x

theorem Complex.sin_sub_two_pi (x : ℂ) :

Complex.sin (x - 2 * ↑Real.pi) = Complex.sin x

theorem Complex.sin_pi_sub (x : ℂ) :

Complex.sin (↑Real.pi - x) = Complex.sin x

theorem Complex.sin_two_pi_sub (x : ℂ) :

Complex.sin (2 * ↑Real.pi - x) = -Complex.sin x

theorem Complex.sin_nat_mul_pi (n : ℕ) :

Complex.sin (↑n * ↑Real.pi) = 0

theorem Complex.sin_int_mul_pi (n : ℤ) :

Complex.sin (↑n * ↑Real.pi) = 0

theorem Complex.sin_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :

Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x

theorem Complex.sin_add_int_mul_two_pi (x : ℂ) (n : ℤ) :

Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x

theorem Complex.sin_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :

Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x

theorem Complex.sin_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :

Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x

theorem Complex.sin_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :

Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x

theorem Complex.sin_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :

Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x

theorem Complex.cos_antiperiodic :

Function.Antiperiodic Complex.cos ↑Real.pi

theorem Complex.cos_periodic :

Function.Periodic Complex.cos (2 * ↑Real.pi)

theorem Complex.cos_add_pi (x : ℂ) :

Complex.cos (x + ↑Real.pi) = -Complex.cos x

theorem Complex.cos_add_two_pi (x : ℂ) :

Complex.cos (x + 2 * ↑Real.pi) = Complex.cos x

theorem Complex.cos_sub_pi (x : ℂ) :

Complex.cos (x - ↑Real.pi) = -Complex.cos x

theorem Complex.cos_sub_two_pi (x : ℂ) :

Complex.cos (x - 2 * ↑Real.pi) = Complex.cos x

theorem Complex.cos_pi_sub (x : ℂ) :

Complex.cos (↑Real.pi - x) = -Complex.cos x

theorem Complex.cos_two_pi_sub (x : ℂ) :

Complex.cos (2 * ↑Real.pi - x) = Complex.cos x

theorem Complex.cos_nat_mul_two_pi (n : ℕ) :

Complex.cos (↑n * (2 * ↑Real.pi)) = 1

theorem Complex.cos_int_mul_two_pi (n : ℤ) :

Complex.cos (↑n * (2 * ↑Real.pi)) = 1

theorem Complex.cos_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :

Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x

theorem Complex.cos_add_int_mul_two_pi (x : ℂ) (n : ℤ) :

Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x

theorem Complex.cos_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :

Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x

theorem Complex.cos_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :

Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x

theorem Complex.cos_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :

Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x

theorem Complex.cos_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :

Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x

theorem Complex.cos_nat_mul_two_pi_add_pi (n : ℕ) :

Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1

theorem Complex.cos_int_mul_two_pi_add_pi (n : ℤ) :

Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1

theorem Complex.cos_nat_mul_two_pi_sub_pi (n : ℕ) :

Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1

theorem Complex.cos_int_mul_two_pi_sub_pi (n : ℤ) :

Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1

theorem Complex.sin_add_pi_div_two (x : ℂ) :

Complex.sin (x + ↑Real.pi / 2) = Complex.cos x

theorem Complex.sin_sub_pi_div_two (x : ℂ) :

Complex.sin (x - ↑Real.pi / 2) = -Complex.cos x

theorem Complex.sin_pi_div_two_sub (x : ℂ) :

Complex.sin (↑Real.pi / 2 - x) = Complex.cos x

theorem Complex.cos_add_pi_div_two (x : ℂ) :

Complex.cos (x + ↑Real.pi / 2) = -Complex.sin x

theorem Complex.cos_sub_pi_div_two (x : ℂ) :

Complex.cos (x - ↑Real.pi / 2) = Complex.sin x

theorem Complex.cos_pi_div_two_sub (x : ℂ) :

Complex.cos (↑Real.pi / 2 - x) = Complex.sin x

theorem Complex.tan_periodic :

Function.Periodic Complex.tan ↑Real.pi

theorem Complex.tan_add_pi (x : ℂ) :

Complex.tan (x + ↑Real.pi) = Complex.tan x

theorem Complex.tan_sub_pi (x : ℂ) :

Complex.tan (x - ↑Real.pi) = Complex.tan x

theorem Complex.tan_pi_sub (x : ℂ) :

Complex.tan (↑Real.pi - x) = -Complex.tan x

theorem Complex.tan_pi_div_two_sub (x : ℂ) :

Complex.tan (↑Real.pi / 2 - x) = (Complex.tan x)⁻¹

theorem Complex.tan_nat_mul_pi (n : ℕ) :

Complex.tan (↑n * ↑Real.pi) = 0

theorem Complex.tan_int_mul_pi (n : ℤ) :

Complex.tan (↑n * ↑Real.pi) = 0

theorem Complex.tan_add_nat_mul_pi (x : ℂ) (n : ℕ) :

Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x

theorem Complex.tan_add_int_mul_pi (x : ℂ) (n : ℤ) :

Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x

theorem Complex.tan_sub_nat_mul_pi (x : ℂ) (n : ℕ) :

Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x

theorem Complex.tan_sub_int_mul_pi (x : ℂ) (n : ℤ) :

Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x

theorem Complex.tan_nat_mul_pi_sub (x : ℂ) (n : ℕ) :

Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x

theorem Complex.tan_int_mul_pi_sub (x : ℂ) (n : ℤ) :

Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x

theorem Complex.exp_antiperiodic :

Function.Antiperiodic Complex.exp (↑Real.pi * Complex.I)

theorem Complex.exp_periodic :

Function.Periodic Complex.exp (2 * ↑Real.pi * Complex.I)

theorem Complex.exp_mul_I_antiperiodic :

Function.Antiperiodic (fun (x : ℂ) => Complex.exp (x * Complex.I)) ↑Real.pi

theorem Complex.exp_mul_I_periodic :

Function.Periodic (fun (x : ℂ) => Complex.exp (x * Complex.I)) (2 * ↑Real.pi)

@[simp]

theorem Complex.exp_pi_mul_I :

Complex.exp (↑Real.pi * Complex.I) = -1

@[simp]

theorem Complex.exp_two_pi_mul_I :

Complex.exp (2 * ↑Real.pi * Complex.I) = 1

@[simp]

theorem Complex.exp_nat_mul_two_pi_mul_I (n : ℕ) :

Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1

@[simp]

theorem Complex.exp_int_mul_two_pi_mul_I (n : ℤ) :

Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1

@[simp]

theorem Complex.exp_add_pi_mul_I (z : ℂ) :

Complex.exp (z + ↑Real.pi * Complex.I) = -Complex.exp z

@[simp]

theorem Complex.exp_sub_pi_mul_I (z : ℂ) :

Complex.exp (z - ↑Real.pi * Complex.I) = -Complex.exp 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 ≤ 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|}}.$$