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.pi / 2).cos = 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 = ⟨Real.pi, 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.pi.sin = 0

@[simp]

theorem Real.cos_pi :

Real.pi.cos = -1

@[simp]

theorem Real.sin_two_pi :

(2 * Real.pi).sin = 0

@[simp]

theorem Real.cos_two_pi :

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

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

@[simp]

theorem Real.sin_add_two_pi (x : ℝ) :

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

@[simp]

theorem Real.sin_sub_pi (x : ℝ) :

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

@[simp]

theorem Real.sin_sub_two_pi (x : ℝ) :

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

@[simp]

theorem Real.sin_pi_sub (x : ℝ) :

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

@[simp]

theorem Real.sin_two_pi_sub (x : ℝ) :

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

@[simp]

theorem Real.sin_nat_mul_pi (n : ℕ) :

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

@[simp]

theorem Real.sin_int_mul_pi (n : ℤ) :

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

(x + ↑n * Real.pi).sin = (-1) ^ n * x.sin

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

(x + ↑n * Real.pi).sin = (-1) ^ n * x.sin

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

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

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

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

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

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

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

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

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 : ℝ) :

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

@[simp]

theorem Real.cos_add_two_pi (x : ℝ) :

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

@[simp]

theorem Real.cos_sub_pi (x : ℝ) :

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

@[simp]

theorem Real.cos_sub_two_pi (x : ℝ) :

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

@[simp]

theorem Real.cos_pi_sub (x : ℝ) :

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

@[simp]

theorem Real.cos_two_pi_sub (x : ℝ) :

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

@[simp]

theorem Real.cos_nat_mul_two_pi (n : ℕ) :

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

@[simp]

theorem Real.cos_int_mul_two_pi (n : ℤ) :

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.cos_nat_mul_two_pi_add_pi (n : ℕ) :

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

theorem Real.cos_int_mul_two_pi_add_pi (n : ℤ) :

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

theorem Real.cos_nat_mul_two_pi_sub_pi (n : ℕ) :

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

theorem Real.cos_int_mul_two_pi_sub_pi (n : ℤ) :

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

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

0 < x.sin

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

0 < x.sin

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

0 ≤ x.sin

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

0 ≤ x.sin

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

x.sin < 0

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

x.sin ≤ 0

@[simp]

theorem Real.sin_pi_div_two :

(Real.pi / 2).sin = 1

theorem Real.sin_add_pi_div_two (x : ℝ) :

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

theorem Real.sin_sub_pi_div_two (x : ℝ) :

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

theorem Real.sin_pi_div_two_sub (x : ℝ) :

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

theorem Real.cos_add_pi_div_two (x : ℝ) :

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

theorem Real.cos_sub_pi_div_two (x : ℝ) :

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

theorem Real.cos_pi_div_two_sub (x : ℝ) :

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

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

0 < x.cos

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

0 ≤ x.cos

theorem Real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : ℝ} (hl : -(Real.pi / 2) ≤ x) (hu : x ≤ Real.pi / 2) :

0 ≤ x.cos

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

x.cos < 0

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

x.cos ≤ 0

theorem Real.sin_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ Real.pi) :

x.sin = √(1 - x.cos ^ 2)

theorem Real.cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(Real.pi / 2) ≤ x) (hu : x ≤ Real.pi / 2) :

x.cos = √(1 - x.sin ^ 2)

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

(x / 2).cos = √((1 + x.cos) / 2)

theorem Real.abs_sin_half (x : ℝ) :

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

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

(x / 2).sin = √((1 - x.cos) / 2)

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

(x / 2).sin = -√((1 - x.cos) / 2)

theorem Real.sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -Real.pi < x) (hx₂ : x < Real.pi) :

x.sin = 0 ↔ x = 0

theorem Real.sin_eq_zero_iff {x : ℝ} :

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

theorem Real.sin_ne_zero_iff {x : ℝ} :

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

theorem Real.sin_eq_zero_iff_cos_eq {x : ℝ} :

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

theorem Real.cos_eq_one_iff (x : ℝ) :

x.cos = 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) :

x.cos = 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) :

x.sin < y.sin

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) :

y.cos < x.cos

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) :

y.cos < x.cos

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) :

y.cos ≤ x.cos

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) :

x.sin ≤ y.sin

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 : ℝ) :

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

theorem Real.cos_mem_Icc (x : ℝ) :

x.cos ∈ 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.range Real.cos).Infinite

theorem Real.range_sin_infinite :

(Set.range Real.sin).Infinite

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

theorem Real.sqrtTwoAddSeries_zero (x : ℝ) :

x.sqrtTwoAddSeries 0 = x

theorem Real.sqrtTwoAddSeries_one :

Real.sqrtTwoAddSeries 0 1 = √2

theorem Real.sqrtTwoAddSeries_two :

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

theorem Real.sqrtTwoAddSeries_zero_nonneg (n : ℕ) :

0 ≤ Real.sqrtTwoAddSeries 0 n

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

0 ≤ x.sqrtTwoAddSeries n

theorem Real.sqrtTwoAddSeries_lt_two (n : ℕ) :

Real.sqrtTwoAddSeries 0 n < 2

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

x.sqrtTwoAddSeries (n + 1) = (√(2 + x)).sqrtTwoAddSeries n

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

x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n

@[simp]

theorem Real.cos_pi_over_two_pow (n : ℕ) :

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

theorem Real.sin_sq_pi_over_two_pow (n : ℕ) :

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

theorem Real.sin_sq_pi_over_two_pow_succ (n : ℕ) :

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

@[simp]

theorem Real.sin_pi_over_two_pow_succ (n : ℕ) :

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

@[simp]

theorem Real.cos_pi_div_four :

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

@[simp]

theorem Real.sin_pi_div_four :

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

@[simp]

theorem Real.cos_pi_div_eight :

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

@[simp]

theorem Real.sin_pi_div_eight :

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

@[simp]

theorem Real.cos_pi_div_sixteen :

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

@[simp]

theorem Real.sin_pi_div_sixteen :

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

@[simp]

theorem Real.cos_pi_div_thirty_two :

(Real.pi / 32).cos = √(2 + √(2 + √(2 + √2))) / 2

@[simp]

theorem Real.sin_pi_div_thirty_two :

(Real.pi / 32).sin = √(2 - √(2 + √(2 + √2))) / 2

@[simp]

theorem Real.cos_pi_div_three :

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

The cosine of π / 3 is 1 / 2.

@[simp]

theorem Real.cos_pi_div_six :

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

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

theorem Real.sq_cos_pi_div_six :

(Real.pi / 6).cos ^ 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.pi / 6).sin = 1 / 2

The sine of π / 6 is 1 / 2.

theorem Real.sq_sin_pi_div_three :

(Real.pi / 3).sin ^ 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.pi / 3).sin = √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) = (↑x).sin

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

Real.sinOrderIso x = ⟨(↑x).sin, ⋯⟩

@[simp]

theorem Real.tan_pi_div_four :

(Real.pi / 4).tan = 1

@[simp]

theorem Real.tan_pi_div_two :

(Real.pi / 2).tan = 0

@[simp]

theorem Real.tan_pi_div_six :

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

@[simp]

theorem Real.tan_pi_div_three :

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

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

0 < x.tan

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

0 ≤ x.tan

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

x.tan < 0

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

x.tan ≤ 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) :

x.tan < y.tan

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) :

x.tan < y.tan

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 : x.tan = y.tan) :

x = y

theorem Real.tan_periodic :

Function.Periodic Real.tan Real.pi

@[simp]

theorem Real.tan_pi :

Real.pi.tan = 0

theorem Real.tan_add_pi (x : ℝ) :

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

theorem Real.tan_sub_pi (x : ℝ) :

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

theorem Real.tan_pi_sub (x : ℝ) :

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

theorem Real.tan_pi_div_two_sub (x : ℝ) :

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

theorem Real.tan_nat_mul_pi (n : ℕ) :

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

theorem Real.tan_int_mul_pi (n : ℤ) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : ℂ} :

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

@[simp]

theorem Complex.cos_pi_div_two :

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

@[simp]

theorem Complex.sin_pi_div_two :

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

@[simp]

theorem Complex.sin_pi :

(↑Real.pi).sin = 0

@[simp]

theorem Complex.cos_pi :

(↑Real.pi).cos = -1

@[simp]

theorem Complex.sin_two_pi :

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

@[simp]

theorem Complex.cos_two_pi :

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

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

theorem Complex.sin_add_two_pi (x : ℂ) :

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

theorem Complex.sin_sub_pi (x : ℂ) :

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

theorem Complex.sin_sub_two_pi (x : ℂ) :

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

theorem Complex.sin_pi_sub (x : ℂ) :

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

theorem Complex.sin_two_pi_sub (x : ℂ) :

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

theorem Complex.sin_nat_mul_pi (n : ℕ) :

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

theorem Complex.sin_int_mul_pi (n : ℤ) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : ℂ) :

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

theorem Complex.cos_add_two_pi (x : ℂ) :

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

theorem Complex.cos_sub_pi (x : ℂ) :

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

theorem Complex.cos_sub_two_pi (x : ℂ) :

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

theorem Complex.cos_pi_sub (x : ℂ) :

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

theorem Complex.cos_two_pi_sub (x : ℂ) :

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

theorem Complex.cos_nat_mul_two_pi (n : ℕ) :

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

theorem Complex.cos_int_mul_two_pi (n : ℤ) :

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Complex.cos_nat_mul_two_pi_add_pi (n : ℕ) :

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

theorem Complex.cos_int_mul_two_pi_add_pi (n : ℤ) :

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

theorem Complex.cos_nat_mul_two_pi_sub_pi (n : ℕ) :

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

theorem Complex.cos_int_mul_two_pi_sub_pi (n : ℤ) :

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

theorem Complex.sin_add_pi_div_two (x : ℂ) :

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

theorem Complex.sin_sub_pi_div_two (x : ℂ) :

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

theorem Complex.sin_pi_div_two_sub (x : ℂ) :

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

theorem Complex.cos_add_pi_div_two (x : ℂ) :

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

theorem Complex.cos_sub_pi_div_two (x : ℂ) :

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

theorem Complex.cos_pi_div_two_sub (x : ℂ) :

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

theorem Complex.tan_periodic :

Function.Periodic Complex.tan ↑Real.pi

theorem Complex.tan_add_pi (x : ℂ) :

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

theorem Complex.tan_sub_pi (x : ℂ) :

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

theorem Complex.tan_pi_sub (x : ℂ) :

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

theorem Complex.tan_pi_div_two_sub (x : ℂ) :

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

theorem Complex.tan_nat_mul_pi (n : ℕ) :

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

theorem Complex.tan_int_mul_pi (n : ℤ) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : ℂ) => (x * Complex.I).exp) ↑Real.pi

theorem Complex.exp_mul_I_periodic :

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

@[simp]

theorem Complex.exp_pi_mul_I :

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

@[simp]

theorem Complex.exp_two_pi_mul_I :

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

@[simp]

theorem Complex.exp_nat_mul_two_pi_mul_I (n : ℕ) :

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

@[simp]

theorem Complex.exp_int_mul_two_pi_mul_I (n : ℤ) :

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

@[simp]

theorem Complex.exp_add_pi_mul_I (z : ℂ) :

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

@[simp]

theorem Complex.exp_sub_pi_mul_I (z : ℂ) :

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

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 (↑a * (z.exp + (-z).exp)).exp ≤ (a * b.cos * |z.re|.exp).exp

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