# 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

source
theorem Complex.continuous_sin :
Continuous sin
source
theorem Complex.continuousOn_sin {s : Set ℂ} :
ContinuousOn sin s
source
theorem Complex.continuous_cos :
Continuous cos
source
theorem Complex.continuousOn_cos {s : Set ℂ} :
ContinuousOn cos s
source
theorem Complex.continuous_sinh :
Continuous sinh
source
theorem Complex.continuous_cosh :
Continuous cosh
source
theorem Real.continuous_sin :
Continuous sin
source
theorem Real.continuousOn_sin {s : Set ℝ} :
ContinuousOn sin s
source
theorem Real.continuous_cos :
Continuous cos
source
theorem Real.continuousOn_cos {s : Set ℝ} :
ContinuousOn cos s
source
theorem Real.continuous_sinh :
Continuous sinh
source
theorem Real.continuous_cosh :
Continuous cosh
source
theorem Real.exists_cos_eq_zero :
0 ∈ cos '' Set.Icc 1 2
source
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 `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.

Equations

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

Instances For

source
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 `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.

Equations

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

Instances For

source
@[simp]
theorem Real.cos_pi_div_two :
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_nonneg :
0 ≤ Real.pi
source
@[simp]
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
def Mathlib.Meta.Positivity.evalRealPi :
PositivityExt

Extension for the `positivity` tactic: `π` is always positive.

Equations

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

Instances For

source
noncomputable def NNReal.pi :
NNReal

`π` considered as a nonnegative real.

Equations

- NNReal.pi = ⟨Real.pi, NNReal.pi._proof_1⟩

Instances For

source
@[simp]
theorem NNReal.coe_real_pi :
↑pi = Real.pi
source
theorem NNReal.pi_pos :
0 < pi
source
theorem NNReal.pi_ne_zero :
pi ≠ 0
source
@[simp]
theorem Real.sin_pi :
sin Real.pi = 0
source
@[simp]
theorem Real.cos_pi :
cos Real.pi = -1
source
@[simp]
theorem Real.sin_two_pi :
sin (2 * Real.pi) = 0
source
@[simp]
theorem Real.cos_two_pi :
cos (2 * Real.pi) = 1
source
theorem Real.sin_antiperiodic :
Function.Antiperiodic sin Real.pi
source
theorem Real.sin_periodic :
Function.Periodic sin (2 * Real.pi)
source
@[simp]
theorem Real.sin_add_pi (x : ℝ) :
sin (x + Real.pi) = -sin x
source
@[simp]
theorem Real.sin_add_two_pi (x : ℝ) :
sin (x + 2 * Real.pi) = sin x
source
@[simp]
theorem Real.sin_sub_pi (x : ℝ) :
sin (x - Real.pi) = -sin x
source
@[simp]
theorem Real.sin_sub_two_pi (x : ℝ) :
sin (x - 2 * Real.pi) = sin x
source
@[simp]
theorem Real.sin_pi_sub (x : ℝ) :
sin (Real.pi - x) = sin x
source
@[simp]
theorem Real.sin_two_pi_sub (x : ℝ) :
sin (2 * Real.pi - x) = -sin x
source
@[simp]
theorem Real.sin_nat_mul_pi (n : ℕ) :
sin (↑n * Real.pi) = 0
source
@[simp]
theorem Real.sin_int_mul_pi (n : ℤ) :
sin (↑n * Real.pi) = 0
source
@[simp]
theorem Real.sin_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :
sin (x + ↑n * (2 * Real.pi)) = sin x
source
@[simp]
theorem Real.sin_add_int_mul_two_pi (x : ℝ) (n : ℤ) :
sin (x + ↑n * (2 * Real.pi)) = sin x
source
@[simp]
theorem Real.sin_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :
sin (x - ↑n * (2 * Real.pi)) = sin x
source
@[simp]
theorem Real.sin_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :
sin (x - ↑n * (2 * Real.pi)) = sin x
source
@[simp]
theorem Real.sin_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :
sin (↑n * (2 * Real.pi) - x) = -sin x
source
@[simp]
theorem Real.sin_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :
sin (↑n * (2 * Real.pi) - x) = -sin x
source
theorem Real.sin_add_int_mul_pi (x : ℝ) (n : ℤ) :
sin (x + ↑n * Real.pi) = (-1) ^ n * sin x
source
theorem Real.sin_add_nat_mul_pi (x : ℝ) (n : ℕ) :
sin (x + ↑n * Real.pi) = (-1) ^ n * sin x
source
theorem Real.sin_sub_int_mul_pi (x : ℝ) (n : ℤ) :
sin (x - ↑n * Real.pi) = (-1) ^ n * sin x
source
theorem Real.sin_sub_nat_mul_pi (x : ℝ) (n : ℕ) :
sin (x - ↑n * Real.pi) = (-1) ^ n * sin x
source
theorem Real.sin_int_mul_pi_sub (x : ℝ) (n : ℤ) :
sin (↑n * Real.pi - x) = -((-1) ^ n * sin x)
source
theorem Real.sin_nat_mul_pi_sub (x : ℝ) (n : ℕ) :
sin (↑n * Real.pi - x) = -((-1) ^ n * sin x)
source
theorem Real.cos_antiperiodic :
Function.Antiperiodic cos Real.pi
source
theorem Real.cos_periodic :
Function.Periodic cos (2 * Real.pi)
source
@[simp]
theorem Real.abs_cos_int_mul_pi (k : ℤ) :
|cos (↑k * Real.pi)| = 1
source
@[simp]
theorem Real.cos_add_pi (x : ℝ) :
cos (x + Real.pi) = -cos x
source
@[simp]
theorem Real.cos_add_two_pi (x : ℝ) :
cos (x + 2 * Real.pi) = cos x
source
@[simp]
theorem Real.cos_sub_pi (x : ℝ) :
cos (x - Real.pi) = -cos x
source
@[simp]
theorem Real.cos_sub_two_pi (x : ℝ) :
cos (x - 2 * Real.pi) = cos x
source
@[simp]
theorem Real.cos_pi_sub (x : ℝ) :
cos (Real.pi - x) = -cos x
source
@[simp]
theorem Real.cos_two_pi_sub (x : ℝ) :
cos (2 * Real.pi - x) = cos x
source
@[simp]
theorem Real.cos_nat_mul_two_pi (n : ℕ) :
cos (↑n * (2 * Real.pi)) = 1
source
@[simp]
theorem Real.cos_int_mul_two_pi (n : ℤ) :
cos (↑n * (2 * Real.pi)) = 1
source
@[simp]
theorem Real.cos_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :
cos (x + ↑n * (2 * Real.pi)) = cos x
source
@[simp]
theorem Real.cos_add_int_mul_two_pi (x : ℝ) (n : ℤ) :
cos (x + ↑n * (2 * Real.pi)) = cos x
source
@[simp]
theorem Real.cos_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :
cos (x - ↑n * (2 * Real.pi)) = cos x
source
@[simp]
theorem Real.cos_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :
cos (x - ↑n * (2 * Real.pi)) = cos x
source
@[simp]
theorem Real.cos_nat_mul_two_pi_sub (x : ℝ) (n : ℕ) :
cos (↑n * (2 * Real.pi) - x) = cos x
source
@[simp]
theorem Real.cos_int_mul_two_pi_sub (x : ℝ) (n : ℤ) :
cos (↑n * (2 * Real.pi) - x) = cos x
source
theorem Real.cos_add_int_mul_pi (x : ℝ) (n : ℤ) :
cos (x + ↑n * Real.pi) = (-1) ^ n * cos x
source
theorem Real.cos_add_nat_mul_pi (x : ℝ) (n : ℕ) :
cos (x + ↑n * Real.pi) = (-1) ^ n * cos x
source
theorem Real.cos_sub_int_mul_pi (x : ℝ) (n : ℤ) :
cos (x - ↑n * Real.pi) = (-1) ^ n * cos x
source
theorem Real.cos_sub_nat_mul_pi (x : ℝ) (n : ℕ) :
cos (x - ↑n * Real.pi) = (-1) ^ n * cos x
source
theorem Real.cos_int_mul_pi_sub (x : ℝ) (n : ℤ) :
cos (↑n * Real.pi - x) = (-1) ^ n * cos x
source
theorem Real.cos_nat_mul_pi_sub (x : ℝ) (n : ℕ) :
cos (↑n * Real.pi - x) = (-1) ^ n * cos x
source
theorem Real.cos_nat_mul_two_pi_add_pi (n : ℕ) :
cos (↑n * (2 * Real.pi) + Real.pi) = -1
source
theorem Real.cos_int_mul_two_pi_add_pi (n : ℤ) :
cos (↑n * (2 * Real.pi) + Real.pi) = -1
source
theorem Real.cos_nat_mul_two_pi_sub_pi (n : ℕ) :
cos (↑n * (2 * Real.pi) - Real.pi) = -1
source
theorem Real.cos_int_mul_two_pi_sub_pi (n : ℤ) :
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 < sin x
source
theorem Real.sin_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo 0 Real.pi) :
0 < sin x
source
theorem Real.sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Set.Icc 0 Real.pi) :
0 ≤ sin x
source
theorem Real.sin_nonneg_of_nonneg_of_le_pi {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ Real.pi) :
0 ≤ sin x
source
theorem Real.sin_neg_of_neg_of_neg_pi_lt {x : ℝ} (hx0 : x < 0) (hpx : -Real.pi < x) :
sin x < 0
source
theorem Real.sin_nonpos_of_nonpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -Real.pi ≤ x) :
sin x ≤ 0
source
@[deprecated Real.sin_nonpos_of_nonpos_of_neg_pi_le (since := "2025-07-27")]
theorem Real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -Real.pi ≤ x) :
sin x ≤ 0

Alias of `Real.sin_nonpos_of_nonpos_of_neg_pi_le`.

source
@[simp]
theorem Real.sin_pi_div_two :
sin (Real.pi / 2) = 1
source
theorem Real.sin_add_pi_div_two (x : ℝ) :
sin (x + Real.pi / 2) = cos x
source
theorem Real.sin_sub_pi_div_two (x : ℝ) :
sin (x - Real.pi / 2) = -cos x
source
theorem Real.sin_pi_div_two_sub (x : ℝ) :
sin (Real.pi / 2 - x) = cos x
source
theorem Real.cos_add_pi_div_two (x : ℝ) :
cos (x + Real.pi / 2) = -sin x
source
theorem Real.cos_sub_pi_div_two (x : ℝ) :
cos (x - Real.pi / 2) = sin x
source
theorem Real.cos_pi_div_two_sub (x : ℝ) :
cos (Real.pi / 2 - x) = sin x
source
theorem Real.cos_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
0 < cos x
source
theorem Real.cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
0 ≤ 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 ≤ 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) :
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) :
cos x ≤ 0
source
theorem Real.sin_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ Real.pi) :
sin x = √(1 - cos x ^ 2)
source
theorem Real.cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(Real.pi / 2) ≤ x) (hu : x ≤ Real.pi / 2) :
cos x = √(1 - sin x ^ 2)
source
theorem Real.cos_half {x : ℝ} (hl : -Real.pi ≤ x) (hr : x ≤ Real.pi) :
cos (x / 2) = √((1 + cos x) / 2)
source
theorem Real.abs_sin_half (x : ℝ) :
|sin (x / 2)| = √((1 - cos x) / 2)
source
theorem Real.sin_half_eq_sqrt {x : ℝ} (hl : 0 ≤ x) (hr : x ≤ 2 * Real.pi) :
sin (x / 2) = √((1 - cos x) / 2)
source
theorem Real.sin_half_eq_neg_sqrt {x : ℝ} (hl : -(2 * Real.pi) ≤ x) (hr : x ≤ 0) :
sin (x / 2) = -√((1 - cos x) / 2)
source
theorem Real.sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -Real.pi < x) (hx₂ : x < Real.pi) :
sin x = 0 ↔ x = 0
source
theorem Real.sin_eq_zero_iff {x : ℝ} :
sin x = 0 ↔ ∃ (n : ℤ), ↑n * Real.pi = x
source
theorem Real.sin_ne_zero_iff {x : ℝ} :
sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * Real.pi ≠ x
source
theorem Real.sin_eq_zero_iff_cos_eq {x : ℝ} :
sin x = 0 ↔ cos x = 1 ∨ cos x = -1
source
theorem Real.cos_eq_zero_iff_sin_eq {x : ℝ} :
cos x = 0 ↔ sin x = 1 ∨ sin x = -1
source
theorem Real.cos_eq_one_iff (x : ℝ) :
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) :
cos x = 1 ↔ x = 0
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) :
sin x < sin y
source
theorem Real.strictMonoOn_sin :
StrictMonoOn sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
source
theorem Real.monotoneOn_sin :
MonotoneOn sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
source
theorem Real.cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ Real.pi) (hxy : x < y) :
cos y < cos x
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) :
cos y < cos x
source
theorem Real.strictAntiOn_cos :
StrictAntiOn cos (Set.Icc 0 Real.pi)
source
theorem Real.antitoneOn_cos :
AntitoneOn 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) :
cos y ≤ cos x
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) :
sin x ≤ sin y
source
theorem Real.injOn_sin :
Set.InjOn sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
source
theorem Real.injOn_cos :
Set.InjOn cos (Set.Icc 0 Real.pi)
source
theorem Real.surjOn_sin :
Set.SurjOn sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
source
theorem Real.surjOn_cos :
Set.SurjOn cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
source
theorem Real.sin_mem_Icc (x : ℝ) :
sin x ∈ Set.Icc (-1) 1
source
theorem Real.cos_mem_Icc (x : ℝ) :
cos x ∈ Set.Icc (-1) 1
source
theorem Real.mapsTo_sin (s : Set ℝ) :
Set.MapsTo sin s (Set.Icc (-1) 1)
source
theorem Real.mapsTo_cos (s : Set ℝ) :
Set.MapsTo cos s (Set.Icc (-1) 1)
source
theorem Real.bijOn_sin :
Set.BijOn sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
source
theorem Real.bijOn_cos :
Set.BijOn cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
source
@[simp]
theorem Real.range_cos :
Set.range cos = Set.Icc (-1) 1
source
@[simp]
theorem Real.range_sin :
Set.range sin = Set.Icc (-1) 1
source
theorem Real.range_cos_infinite :
(Set.range cos).Infinite
source
theorem Real.range_sin_infinite :
(Set.range sin).Infinite
source
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

- x.sqrtTwoAddSeries 0 = x
- x.sqrtTwoAddSeries n.succ = √(2 + x.sqrtTwoAddSeries n)

Instances For

source
theorem Real.sqrtTwoAddSeries_zero (x : ℝ) :
x.sqrtTwoAddSeries 0 = x
source
theorem Real.sqrtTwoAddSeries_one :
sqrtTwoAddSeries 0 1 = √2
source
theorem Real.sqrtTwoAddSeries_two :
sqrtTwoAddSeries 0 2 = √(2 + √2)
source
theorem Real.sqrtTwoAddSeries_zero_nonneg (n : ℕ) :
0 ≤ sqrtTwoAddSeries 0 n
source
theorem Real.sqrtTwoAddSeries_nonneg {x : ℝ} (h : 0 ≤ x) (n : ℕ) :
0 ≤ x.sqrtTwoAddSeries n
source
theorem Real.sqrtTwoAddSeries_lt_two (n : ℕ) :
sqrtTwoAddSeries 0 n < 2
source
theorem Real.sqrtTwoAddSeries_succ (x : ℝ) (n : ℕ) :
x.sqrtTwoAddSeries (n + 1) = (√(2 + x)).sqrtTwoAddSeries n
source
theorem Real.sqrtTwoAddSeries_monotone_left {x y : ℝ} (h : x ≤ y) (n : ℕ) :
x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
source
@[simp]
theorem Real.cos_pi_over_two_pow (n : ℕ) :
cos (Real.pi / 2 ^ (n + 1)) = sqrtTwoAddSeries 0 n / 2
source
theorem Real.sin_sq_pi_over_two_pow (n : ℕ) :
sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2
source
theorem Real.sin_sq_pi_over_two_pow_succ (n : ℕ) :
sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
source
@[simp]
theorem Real.sin_pi_over_two_pow_succ (n : ℕ) :
sin (Real.pi / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2
source
@[simp]
theorem Real.cos_pi_div_four :
cos (Real.pi / 4) = √2 / 2
source
@[simp]
theorem Real.sin_pi_div_four :
sin (Real.pi / 4) = √2 / 2
source
@[simp]
theorem Real.cos_pi_div_eight :
cos (Real.pi / 8) = √(2 + √2) / 2
source
@[simp]
theorem Real.sin_pi_div_eight :
sin (Real.pi / 8) = √(2 - √2) / 2
source
@[simp]
theorem Real.cos_pi_div_sixteen :
cos (Real.pi / 16) = √(2 + √(2 + √2)) / 2
source
@[simp]
theorem Real.sin_pi_div_sixteen :
sin (Real.pi / 16) = √(2 - √(2 + √2)) / 2
source
@[simp]
theorem Real.cos_pi_div_thirty_two :
cos (Real.pi / 32) = √(2 + √(2 + √(2 + √2))) / 2
source
@[simp]
theorem Real.sin_pi_div_thirty_two :
sin (Real.pi / 32) = √(2 - √(2 + √(2 + √2))) / 2
source
@[simp]
theorem Real.cos_pi_div_three :
cos (Real.pi / 3) = 1 / 2

The cosine of `π / 3` is `1 / 2`.

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

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

source
theorem Real.sq_cos_pi_div_six :
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.sin_pi_div_six :
sin (Real.pi / 6) = 1 / 2

The sine of `π / 6` is `1 / 2`.

source
theorem Real.sq_sin_pi_div_three :
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 :
sin (Real.pi / 3) = √3 / 2

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

source
theorem Real.quadratic_root_cos_pi_div_five :
4 * cos (Real.pi / 5) ^ 2 - 2 * cos (Real.pi / 5) - 1 = 0
source
theorem Real.Polynomial.isRoot_cos_pi_div_five :
(4 • Polynomial.X ^ 2 - 2 • Polynomial.X - Polynomial.C 1).IsRoot (cos (Real.pi / 5))
source
@[simp]
theorem Real.cos_pi_div_five :
cos (Real.pi / 5) = (1 + √5) / 4

The cosine of `π / 5` is `(1 + √5) / 4`.

source
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

source
@[simp]
theorem Real.coe_sinOrderIso_apply (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :
↑(sinOrderIso x) = sin ↑x
source
theorem Real.sinOrderIso_apply (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :
sinOrderIso x = ⟨sin ↑x, ⋯⟩
source
@[simp]
theorem Real.tan_pi_div_four :
tan (Real.pi / 4) = 1
source
@[simp]
theorem Real.tan_pi_div_two :
tan (Real.pi / 2) = 0
source
@[simp]
theorem Real.tan_pi_div_six :
tan (Real.pi / 6) = 1 / √3
source
@[simp]
theorem Real.tan_pi_div_three :
tan (Real.pi / 3) = √3
source
theorem Real.tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < Real.pi / 2) :
0 < tan x
source
theorem Real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ Real.pi / 2) :
0 ≤ tan x
source
theorem Real.tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(Real.pi / 2) < x) :
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) :
tan x ≤ 0
source
theorem Real.strictMonoOn_tan :
StrictMonoOn tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
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) :
tan x < tan y
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) :
tan x < tan y
source
theorem Real.injOn_tan :
Set.InjOn 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 : tan x = tan y) :
x = y
source
theorem Real.tan_periodic :
Function.Periodic tan Real.pi
source
@[simp]
theorem Real.tan_pi :
tan Real.pi = 0
source
theorem Real.tan_add_pi (x : ℝ) :
tan (x + Real.pi) = tan x
source
theorem Real.tan_sub_pi (x : ℝ) :
tan (x - Real.pi) = tan x
source
theorem Real.tan_pi_sub (x : ℝ) :
tan (Real.pi - x) = -tan x
source
theorem Real.tan_pi_div_two_sub (x : ℝ) :
tan (Real.pi / 2 - x) = (tan x)⁻¹
source
theorem Real.tan_nat_mul_pi (n : ℕ) :
tan (↑n * Real.pi) = 0
source
theorem Real.tan_int_mul_pi (n : ℤ) :
tan (↑n * Real.pi) = 0
source
theorem Real.tan_add_nat_mul_pi (x : ℝ) (n : ℕ) :
tan (x + ↑n * Real.pi) = tan x
source
theorem Real.tan_add_int_mul_pi (x : ℝ) (n : ℤ) :
tan (x + ↑n * Real.pi) = tan x
source
theorem Real.tan_sub_nat_mul_pi (x : ℝ) (n : ℕ) :
tan (x - ↑n * Real.pi) = tan x
source
theorem Real.tan_sub_int_mul_pi (x : ℝ) (n : ℤ) :
tan (x - ↑n * Real.pi) = tan x
source
theorem Real.tan_nat_mul_pi_sub (x : ℝ) (n : ℕ) :
tan (↑n * Real.pi - x) = -tan x
source
theorem Real.tan_int_mul_pi_sub (x : ℝ) (n : ℤ) :
tan (↑n * Real.pi - x) = -tan x
source
theorem Real.tendsto_sin_pi_div_two :
Filter.Tendsto sin (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhds 1)
source
theorem Real.tendsto_cos_pi_div_two :
Filter.Tendsto cos (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhdsWithin 0 (Set.Ioi 0))
source
theorem Real.tendsto_tan_pi_div_two :
Filter.Tendsto tan (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) Filter.atTop
source
theorem Real.tendsto_sin_neg_pi_div_two :
Filter.Tendsto sin (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhds (-1))
source
theorem Real.tendsto_cos_neg_pi_div_two :
Filter.Tendsto cos (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhdsWithin 0 (Set.Ioi 0))
source
theorem Real.tendsto_tan_neg_pi_div_two :
Filter.Tendsto tan (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) Filter.atBot
source
theorem Complex.sin_eq_zero_iff_cos_eq {z : ℂ} :
sin z = 0 ↔ cos z = 1 ∨ cos z = -1
source
theorem Complex.cos_eq_zero_iff_sin_eq {z : ℂ} :
cos z = 0 ↔ sin z = 1 ∨ sin z = -1
source
@[simp]
theorem Complex.cos_pi_div_two :
cos (↑Real.pi / 2) = 0
source
@[simp]
theorem Complex.sin_pi_div_two :
sin (↑Real.pi / 2) = 1
source
@[simp]
theorem Complex.sin_pi :
sin ↑Real.pi = 0
source
@[simp]
theorem Complex.cos_pi :
cos ↑Real.pi = -1
source
@[simp]
theorem Complex.sin_two_pi :
sin (2 * ↑Real.pi) = 0
source
@[simp]
theorem Complex.cos_two_pi :
cos (2 * ↑Real.pi) = 1
source
theorem Complex.sin_antiperiodic :
Function.Antiperiodic sin ↑Real.pi
source
theorem Complex.sin_periodic :
Function.Periodic sin (2 * ↑Real.pi)
source
theorem Complex.sin_add_pi (x : ℂ) :
sin (x + ↑Real.pi) = -sin x
source
theorem Complex.sin_add_two_pi (x : ℂ) :
sin (x + 2 * ↑Real.pi) = sin x
source
theorem Complex.sin_sub_pi (x : ℂ) :
sin (x - ↑Real.pi) = -sin x
source
theorem Complex.sin_sub_two_pi (x : ℂ) :
sin (x - 2 * ↑Real.pi) = sin x
source
theorem Complex.sin_pi_sub (x : ℂ) :
sin (↑Real.pi - x) = sin x
source
theorem Complex.sin_two_pi_sub (x : ℂ) :
sin (2 * ↑Real.pi - x) = -sin x
source
theorem Complex.sin_nat_mul_pi (n : ℕ) :
sin (↑n * ↑Real.pi) = 0
source
theorem Complex.sin_int_mul_pi (n : ℤ) :
sin (↑n * ↑Real.pi) = 0
source
theorem Complex.sin_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :
sin (x + ↑n * (2 * ↑Real.pi)) = sin x
source
theorem Complex.sin_add_int_mul_two_pi (x : ℂ) (n : ℤ) :
sin (x + ↑n * (2 * ↑Real.pi)) = sin x
source
theorem Complex.sin_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :
sin (x - ↑n * (2 * ↑Real.pi)) = sin x
source
theorem Complex.sin_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :
sin (x - ↑n * (2 * ↑Real.pi)) = sin x
source
theorem Complex.sin_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :
sin (↑n * (2 * ↑Real.pi) - x) = -sin x
source
theorem Complex.sin_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :
sin (↑n * (2 * ↑Real.pi) - x) = -sin x
source
theorem Complex.cos_antiperiodic :
Function.Antiperiodic cos ↑Real.pi
source
theorem Complex.cos_periodic :
Function.Periodic cos (2 * ↑Real.pi)
source
theorem Complex.cos_add_pi (x : ℂ) :
cos (x + ↑Real.pi) = -cos x
source
theorem Complex.cos_add_two_pi (x : ℂ) :
cos (x + 2 * ↑Real.pi) = cos x
source
theorem Complex.cos_sub_pi (x : ℂ) :
cos (x - ↑Real.pi) = -cos x
source
theorem Complex.cos_sub_two_pi (x : ℂ) :
cos (x - 2 * ↑Real.pi) = cos x
source
theorem Complex.cos_pi_sub (x : ℂ) :
cos (↑Real.pi - x) = -cos x
source
theorem Complex.cos_two_pi_sub (x : ℂ) :
cos (2 * ↑Real.pi - x) = cos x
source
theorem Complex.cos_nat_mul_two_pi (n : ℕ) :
cos (↑n * (2 * ↑Real.pi)) = 1
source
theorem Complex.cos_int_mul_two_pi (n : ℤ) :
cos (↑n * (2 * ↑Real.pi)) = 1
source
theorem Complex.cos_add_nat_mul_two_pi (x : ℂ) (n : ℕ) :
cos (x + ↑n * (2 * ↑Real.pi)) = cos x
source
theorem Complex.cos_add_int_mul_two_pi (x : ℂ) (n : ℤ) :
cos (x + ↑n * (2 * ↑Real.pi)) = cos x
source
theorem Complex.cos_sub_nat_mul_two_pi (x : ℂ) (n : ℕ) :
cos (x - ↑n * (2 * ↑Real.pi)) = cos x
source
theorem Complex.cos_sub_int_mul_two_pi (x : ℂ) (n : ℤ) :
cos (x - ↑n * (2 * ↑Real.pi)) = cos x
source
theorem Complex.cos_nat_mul_two_pi_sub (x : ℂ) (n : ℕ) :
cos (↑n * (2 * ↑Real.pi) - x) = cos x
source
theorem Complex.cos_int_mul_two_pi_sub (x : ℂ) (n : ℤ) :
cos (↑n * (2 * ↑Real.pi) - x) = cos x
source
theorem Complex.cos_nat_mul_two_pi_add_pi (n : ℕ) :
cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
source
theorem Complex.cos_int_mul_two_pi_add_pi (n : ℤ) :
cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
source
theorem Complex.cos_nat_mul_two_pi_sub_pi (n : ℕ) :
cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
source
theorem Complex.cos_int_mul_two_pi_sub_pi (n : ℤ) :
cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
source
theorem Complex.sin_add_pi_div_two (x : ℂ) :
sin (x + ↑Real.pi / 2) = cos x
source
theorem Complex.sin_sub_pi_div_two (x : ℂ) :
sin (x - ↑Real.pi / 2) = -cos x
source
theorem Complex.sin_pi_div_two_sub (x : ℂ) :
sin (↑Real.pi / 2 - x) = cos x
source
theorem Complex.cos_add_pi_div_two (x : ℂ) :
cos (x + ↑Real.pi / 2) = -sin x
source
theorem Complex.cos_sub_pi_div_two (x : ℂ) :
cos (x - ↑Real.pi / 2) = sin x
source
theorem Complex.cos_pi_div_two_sub (x : ℂ) :
cos (↑Real.pi / 2 - x) = sin x
source
theorem Complex.tan_periodic :
Function.Periodic tan ↑Real.pi
source
theorem Complex.tan_add_pi (x : ℂ) :
tan (x + ↑Real.pi) = tan x
source
theorem Complex.tan_sub_pi (x : ℂ) :
tan (x - ↑Real.pi) = tan x
source
theorem Complex.tan_pi_sub (x : ℂ) :
tan (↑Real.pi - x) = -tan x
source
theorem Complex.tan_pi_div_two_sub (x : ℂ) :
tan (↑Real.pi / 2 - x) = (tan x)⁻¹
source
theorem Complex.tan_nat_mul_pi (n : ℕ) :
tan (↑n * ↑Real.pi) = 0
source
theorem Complex.tan_int_mul_pi (n : ℤ) :
tan (↑n * ↑Real.pi) = 0
source
theorem Complex.tan_add_nat_mul_pi (x : ℂ) (n : ℕ) :
tan (x + ↑n * ↑Real.pi) = tan x
source
theorem Complex.tan_add_int_mul_pi (x : ℂ) (n : ℤ) :
tan (x + ↑n * ↑Real.pi) = tan x
source
theorem Complex.tan_sub_nat_mul_pi (x : ℂ) (n : ℕ) :
tan (x - ↑n * ↑Real.pi) = tan x
source
theorem Complex.tan_sub_int_mul_pi (x : ℂ) (n : ℤ) :
tan (x - ↑n * ↑Real.pi) = tan x
source
theorem Complex.tan_nat_mul_pi_sub (x : ℂ) (n : ℕ) :
tan (↑n * ↑Real.pi - x) = -tan x
source
theorem Complex.tan_int_mul_pi_sub (x : ℂ) (n : ℤ) :
tan (↑n * ↑Real.pi - x) = -tan x
source
theorem Complex.exp_antiperiodic :
Function.Antiperiodic exp (↑Real.pi * I)
source
theorem Complex.exp_periodic :
Function.Periodic exp (2 * ↑Real.pi * I)
source
theorem Complex.exp_mul_I_antiperiodic :
Function.Antiperiodic (fun (x : ℂ) => exp (x * I)) ↑Real.pi
source
theorem Complex.exp_mul_I_periodic :
Function.Periodic (fun (x : ℂ) => exp (x * I)) (2 * ↑Real.pi)
source
@[simp]
theorem Complex.exp_pi_mul_I :
exp (↑Real.pi * I) = -1
source
@[simp]
theorem Complex.exp_two_pi_mul_I :
exp (2 * ↑Real.pi * I) = 1
source
@[simp]
theorem Complex.exp_pi_div_two_mul_I :
exp (↑Real.pi / 2 * I) = I
source
@[simp]
theorem Complex.exp_neg_pi_div_two_mul_I :
exp (-↑Real.pi / 2 * I) = -I
source
@[simp]
theorem Complex.exp_nat_mul_two_pi_mul_I (n : ℕ) :
exp (↑n * (2 * ↑Real.pi * I)) = 1
source
@[simp]
theorem Complex.exp_int_mul_two_pi_mul_I (n : ℤ) :
exp (↑n * (2 * ↑Real.pi * I)) = 1
source
@[simp]
theorem Complex.exp_add_pi_mul_I (z : ℂ) :
exp (z + ↑Real.pi * I) = -exp z
source
@[simp]
theorem Complex.exp_sub_pi_mul_I (z : ℂ) :
exp (z - ↑Real.pi * I) = -exp z
source
theorem Complex.norm_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) :
‖exp (↑a * (exp z + 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|}}.$$