mathlib documentation

analysis.special_functions.trigonometric

Trigonometric functions

Main definitions

This file contains the following definitions:

Main statements

Many basic inequalities on trigonometric functions are established.

The continuity and differentiability of the usual trigonometric functions are proved, and their derivatives are computed.

Tags

log, sin, cos, tan, arcsin, arccos, arctan, angle, argument

source
theorem complex.has_deriv_at_sin (x : ℂ) :
has_deriv_at complex.sin (complex.cos x) x

The complex sine function is everywhere differentiable, with the derivative cos x.

source
theorem complex.differentiable_sin  :
differentiable ℂ complex.sin

source
theorem complex.differentiable_at_sin {x : ℂ} :
differentiable_at ℂ complex.sin x

source
@[simp]
theorem complex.deriv_sin  :
deriv complex.sin = complex.cos

source
theorem complex.continuous_sin  :
continuous complex.sin

source
theorem complex.continuous_on_sin {s : set ℂ} :
continuous_on complex.sin s

source
theorem complex.measurable_sin  :
measurable complex.sin

source
theorem complex.has_deriv_at_cos (x : ℂ) :
has_deriv_at complex.cos (-complex.sin x) x

The complex cosine function is everywhere differentiable, with the derivative -sin x.

source
theorem complex.differentiable_cos  :
differentiable ℂ complex.cos

source
theorem complex.differentiable_at_cos {x : ℂ} :
differentiable_at ℂ complex.cos x

source
theorem complex.deriv_cos {x : ℂ} :
deriv complex.cos x = -complex.sin x

source
@[simp]
theorem complex.deriv_cos'  :
deriv complex.cos = λ (x : ℂ), -complex.sin x

source
theorem complex.continuous_cos  :
continuous complex.cos

source
theorem complex.continuous_on_cos {s : set ℂ} :
continuous_on complex.cos s

source
theorem complex.measurable_cos  :
measurable complex.cos

source
theorem complex.has_deriv_at_sinh (x : ℂ) :
has_deriv_at complex.sinh (complex.cosh x) x

The complex hyperbolic sine function is everywhere differentiable, with the derivative cosh x.

source
theorem complex.differentiable_sinh  :
differentiable ℂ complex.sinh

source
theorem complex.differentiable_at_sinh {x : ℂ} :
differentiable_at ℂ complex.sinh x

source
@[simp]
theorem complex.deriv_sinh  :
deriv complex.sinh = complex.cosh

source
theorem complex.continuous_sinh  :
continuous complex.sinh

source
theorem complex.measurable_sinh  :
measurable complex.sinh

source
theorem complex.has_deriv_at_cosh (x : ℂ) :
has_deriv_at complex.cosh (complex.sinh x) x

The complex hyperbolic cosine function is everywhere differentiable, with the derivative sinh x.

source
theorem complex.differentiable_cosh  :
differentiable ℂ complex.cosh

source
theorem complex.differentiable_at_cosh {x : ℂ} :
differentiable_at ℂ complex.cos x

source
@[simp]
theorem complex.deriv_cosh  :
deriv complex.cosh = complex.sinh

source
theorem complex.continuous_cosh  :
continuous complex.cosh

source
theorem complex.measurable_cosh  :
measurable complex.cosh

Register lemmas for the derivatives of the composition of complex.cos, complex.sin, complex.cosh and complex.sinh with a differentiable function, for standalone use and use with simp.

complex.cos

source
theorem measurable.ccos {f : ℂ → ℂ} :
measurable f → measurable (λ (x : ℂ), complex.cos (f x))

source
theorem has_deriv_at.ccos {f : ℂ → ℂ} {f' x : ℂ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℂ), complex.cos (f x)) ((-complex.sin (f x)) * f') x

source
theorem has_deriv_within_at.ccos {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℂ), complex.cos (f x)) ((-complex.sin (f x)) * f') s x

source
theorem differentiable_within_at.ccos {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → differentiable_within_at ℂ (λ (x : ℂ), complex.cos (f x)) s x

source
@[simp]
theorem differentiable_at.ccos {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.cos (f x)) x

source
theorem differentiable_on.ccos {f : ℂ → ℂ} {s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.cos (f x)) s

source
@[simp]
theorem differentiable.ccos {f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.cos (f x))

source
theorem deriv_within_ccos {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → unique_diff_within_at ℂ s x → deriv_within (λ (x : ℂ), complex.cos (f x)) s x = (-complex.sin (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_ccos {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.cos (f x)) x = (-complex.sin (f x)) * deriv f x

complex.sin

source
theorem measurable.csin {f : ℂ → ℂ} :
measurable f → measurable (λ (x : ℂ), complex.sin (f x))

source
theorem has_deriv_at.csin {f : ℂ → ℂ} {f' x : ℂ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℂ), complex.sin (f x)) ((complex.cos (f x)) * f') x

source
theorem has_deriv_within_at.csin {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℂ), complex.sin (f x)) ((complex.cos (f x)) * f') s x

source
theorem differentiable_within_at.csin {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → differentiable_within_at ℂ (λ (x : ℂ), complex.sin (f x)) s x

source
@[simp]
theorem differentiable_at.csin {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.sin (f x)) x

source
theorem differentiable_on.csin {f : ℂ → ℂ} {s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.sin (f x)) s

source
@[simp]
theorem differentiable.csin {f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.sin (f x))

source
theorem deriv_within_csin {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → unique_diff_within_at ℂ s x → deriv_within (λ (x : ℂ), complex.sin (f x)) s x = (complex.cos (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_csin {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.sin (f x)) x = (complex.cos (f x)) * deriv f x

complex.cosh

source
theorem measurable.ccosh {f : ℂ → ℂ} :
measurable f → measurable (λ (x : ℂ), complex.cosh (f x))

source
theorem has_deriv_at.ccosh {f : ℂ → ℂ} {f' x : ℂ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℂ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x

source
theorem has_deriv_within_at.ccosh {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℂ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x

source
theorem differentiable_within_at.ccosh {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → differentiable_within_at ℂ (λ (x : ℂ), complex.cosh (f x)) s x

source
@[simp]
theorem differentiable_at.ccosh {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.cosh (f x)) x

source
theorem differentiable_on.ccosh {f : ℂ → ℂ} {s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.cosh (f x)) s

source
@[simp]
theorem differentiable.ccosh {f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.cosh (f x))

source
theorem deriv_within_ccosh {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → unique_diff_within_at ℂ s x → deriv_within (λ (x : ℂ), complex.cosh (f x)) s x = (complex.sinh (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_ccosh {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.cosh (f x)) x = (complex.sinh (f x)) * deriv f x

complex.sinh

source
theorem measurable.csinh {f : ℂ → ℂ} :
measurable f → measurable (λ (x : ℂ), complex.sinh (f x))

source
theorem has_deriv_at.csinh {f : ℂ → ℂ} {f' x : ℂ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℂ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x

source
theorem has_deriv_within_at.csinh {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℂ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x

source
theorem differentiable_within_at.csinh {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → differentiable_within_at ℂ (λ (x : ℂ), complex.sinh (f x)) s x

source
@[simp]
theorem differentiable_at.csinh {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.sinh (f x)) x

source
theorem differentiable_on.csinh {f : ℂ → ℂ} {s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.sinh (f x)) s

source
@[simp]
theorem differentiable.csinh {f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.sinh (f x))

source
theorem deriv_within_csinh {f : ℂ → ℂ} {x : ℂ} {s : set ℂ} :
differentiable_within_at ℂ f s x → unique_diff_within_at ℂ s x → deriv_within (λ (x : ℂ), complex.sinh (f x)) s x = (complex.cosh (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_csinh {f : ℂ → ℂ} {x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.sinh (f x)) x = (complex.cosh (f x)) * deriv f x

source
theorem real.has_deriv_at_sin (x : ℝ) :
has_deriv_at real.sin (real.cos x) x

source
theorem real.differentiable_sin  :
differentiable ℝ real.sin

source
theorem real.differentiable_at_sin {x : ℝ} :
differentiable_at ℝ real.sin x

source
@[simp]
theorem real.deriv_sin  :
deriv real.sin = real.cos

source
theorem real.continuous_sin  :
continuous real.sin

source
theorem real.measurable_sin  :
measurable real.sin

source
theorem real.has_deriv_at_cos (x : ℝ) :
has_deriv_at real.cos (-real.sin x) x

source
theorem real.differentiable_cos  :
differentiable ℝ real.cos

source
theorem real.differentiable_at_cos {x : ℝ} :
differentiable_at ℝ real.cos x

source
theorem real.deriv_cos {x : ℝ} :
deriv real.cos x = -real.sin x

source
@[simp]
theorem real.deriv_cos'  :
deriv real.cos = λ (x : ℝ), -real.sin x

source
theorem real.continuous_cos  :
continuous real.cos

source
theorem real.continuous_on_cos {s : set ℝ} :
continuous_on real.cos s

source
theorem real.measurable_cos  :
measurable real.cos

source
theorem real.has_deriv_at_sinh (x : ℝ) :
has_deriv_at real.sinh (real.cosh x) x

source
theorem real.differentiable_sinh  :
differentiable ℝ real.sinh

source
theorem real.differentiable_at_sinh {x : ℝ} :
differentiable_at ℝ real.sinh x

source
@[simp]
theorem real.deriv_sinh  :
deriv real.sinh = real.cosh

source
theorem real.continuous_sinh  :
continuous real.sinh

source
theorem real.measurable_sinh  :
measurable real.sinh

source
theorem real.has_deriv_at_cosh (x : ℝ) :
has_deriv_at real.cosh (real.sinh x) x

source
theorem real.differentiable_cosh  :
differentiable ℝ real.cosh

source
theorem real.differentiable_at_cosh {x : ℝ} :
differentiable_at ℝ real.cosh x

source
@[simp]
theorem real.deriv_cosh  :
deriv real.cosh = real.sinh

source
theorem real.continuous_cosh  :
continuous real.cosh

source
theorem real.measurable_cosh  :
measurable real.cosh

source
theorem real.sinh_strict_mono  :
strict_mono real.sinh

sinh is strictly monotone.

Register lemmas for the derivatives of the composition of real.exp, real.cos, real.sin, real.cosh and real.sinh with a differentiable function, for standalone use and use with simp.

real.cos

source
theorem measurable.cos {f : ℝ → ℝ} :
measurable f → measurable (λ (x : ℝ), real.cos (f x))

source
theorem has_deriv_at.cos {f : ℝ → ℝ} {f' x : ℝ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℝ), real.cos (f x)) ((-real.sin (f x)) * f') x

source
theorem has_deriv_within_at.cos {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℝ), real.cos (f x)) ((-real.sin (f x)) * f') s x

source
theorem differentiable_within_at.cos {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → differentiable_within_at ℝ (λ (x : ℝ), real.cos (f x)) s x

source
@[simp]
theorem differentiable_at.cos {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.cos (f x)) x

source
theorem differentiable_on.cos {f : ℝ → ℝ} {s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.cos (f x)) s

source
@[simp]
theorem differentiable.cos {f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.cos (f x))

source
theorem deriv_within_cos {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), real.cos (f x)) s x = (-real.sin (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_cos {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → deriv (λ (x : ℝ), real.cos (f x)) x = (-real.sin (f x)) * deriv f x

real.sin

source
theorem measurable.sin {f : ℝ → ℝ} :
measurable f → measurable (λ (x : ℝ), real.sin (f x))

source
theorem has_deriv_at.sin {f : ℝ → ℝ} {f' x : ℝ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℝ), real.sin (f x)) ((real.cos (f x)) * f') x

source
theorem has_deriv_within_at.sin {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℝ), real.sin (f x)) ((real.cos (f x)) * f') s x

source
theorem differentiable_within_at.sin {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → differentiable_within_at ℝ (λ (x : ℝ), real.sin (f x)) s x

source
@[simp]
theorem differentiable_at.sin {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.sin (f x)) x

source
theorem differentiable_on.sin {f : ℝ → ℝ} {s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.sin (f x)) s

source
@[simp]
theorem differentiable.sin {f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.sin (f x))

source
theorem deriv_within_sin {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), real.sin (f x)) s x = (real.cos (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_sin {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → deriv (λ (x : ℝ), real.sin (f x)) x = (real.cos (f x)) * deriv f x

real.cosh

source
theorem measurable.cosh {f : ℝ → ℝ} :
measurable f → measurable (λ (x : ℝ), real.cosh (f x))

source
theorem has_deriv_at.cosh {f : ℝ → ℝ} {f' x : ℝ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℝ), real.cosh (f x)) ((real.sinh (f x)) * f') x

source
theorem has_deriv_within_at.cosh {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℝ), real.cosh (f x)) ((real.sinh (f x)) * f') s x

source
theorem differentiable_within_at.cosh {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → differentiable_within_at ℝ (λ (x : ℝ), real.cosh (f x)) s x

source
@[simp]
theorem differentiable_at.cosh {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.cosh (f x)) x

source
theorem differentiable_on.cosh {f : ℝ → ℝ} {s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.cosh (f x)) s

source
@[simp]
theorem differentiable.cosh {f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.cosh (f x))

source
theorem deriv_within_cosh {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), real.cosh (f x)) s x = (real.sinh (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_cosh {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → deriv (λ (x : ℝ), real.cosh (f x)) x = (real.sinh (f x)) * deriv f x

real.sinh

source
theorem measurable.sinh {f : ℝ → ℝ} :
measurable f → measurable (λ (x : ℝ), real.sinh (f x))

source
theorem has_deriv_at.sinh {f : ℝ → ℝ} {f' x : ℝ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℝ), real.sinh (f x)) ((real.cosh (f x)) * f') x

source
theorem has_deriv_within_at.sinh {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℝ), real.sinh (f x)) ((real.cosh (f x)) * f') s x

source
theorem differentiable_within_at.sinh {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → differentiable_within_at ℝ (λ (x : ℝ), real.sinh (f x)) s x

source
@[simp]
theorem differentiable_at.sinh {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.sinh (f x)) x

source
theorem differentiable_on.sinh {f : ℝ → ℝ} {s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.sinh (f x)) s

source
@[simp]
theorem differentiable.sinh {f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.sinh (f x))

source
theorem deriv_within_sinh {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), real.sinh (f x)) s x = (real.cosh (f x)) * deriv_within f s x

source
@[simp]
theorem deriv_sinh {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → deriv (λ (x : ℝ), real.sinh (f x)) x = (real.cosh (f x)) * deriv f x

source
theorem real.exists_cos_eq_zero  :
0 ∈ real.cos '' set.Icc 1 2

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

Equations
source
@[simp]
theorem real.cos_pi_div_two  :
real.cos (π / 2) = 0

source
theorem real.one_le_pi_div_two  :
1 ≤ π / 2

source
theorem real.pi_div_two_le_two  :
π / 2 ≤ 2

source
theorem real.two_le_pi  :
2 ≤ π

source
theorem real.pi_le_four  :
π ≤ 4

source
theorem real.pi_pos  :
0 < π

source
theorem real.pi_ne_zero  :
π ≠ 0

source
theorem real.pi_div_two_pos  :
0 < π / 2

source
theorem real.two_pi_pos  :
0 < 2 * π

source
@[simp]
theorem real.sin_pi  :
real.sin π = 0

source
@[simp]
theorem real.cos_pi  :
real.cos π = -1

source
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * π) = 0

source
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * π) = 1

source
theorem real.sin_add_pi (x : ℝ) :
real.sin (x + π) = -real.sin x

source
theorem real.sin_add_two_pi (x : ℝ) :
real.sin (x + 2 * π) = real.sin x

source
theorem real.cos_add_two_pi (x : ℝ) :
real.cos (x + 2 * π) = real.cos x

source
theorem real.sin_pi_sub (x : ℝ) :
real.sin (π - x) = real.sin x

source
theorem real.cos_add_pi (x : ℝ) :
real.cos (x + π) = -real.cos x

source
theorem real.cos_pi_sub (x : ℝ) :
real.cos (π - x) = -real.cos x

source
theorem real.sin_pos_of_pos_of_lt_pi {x : ℝ} :
0 < x → x < π → 0 < real.sin x

source
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : ℝ} :
0 ≤ x → x ≤ π → 0 ≤ real.sin x

source
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : ℝ} :
x < 0 → -π < x → real.sin x < 0

source
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : ℝ} :
x ≤ 0 → -π ≤ x → real.sin x ≤ 0

source
@[simp]
theorem real.sin_pi_div_two  :
real.sin (π / 2) = 1

source
theorem real.sin_add_pi_div_two (x : ℝ) :
real.sin (x + π / 2) = real.cos x

source
theorem real.sin_sub_pi_div_two (x : ℝ) :
real.sin (x - π / 2) = -real.cos x

source
theorem real.sin_pi_div_two_sub (x : ℝ) :
real.sin (π / 2 - x) = real.cos x

source
theorem real.cos_add_pi_div_two (x : ℝ) :
real.cos (x + π / 2) = -real.sin x

source
theorem real.cos_sub_pi_div_two (x : ℝ) :
real.cos (x - π / 2) = real.sin x

source
theorem real.cos_pi_div_two_sub (x : ℝ) :
real.cos (π / 2 - x) = real.sin x

source
theorem real.cos_pos_of_mem_Ioo {x : ℝ} :
-(π / 2) < x → x < π / 2 → 0 < real.cos x

source
theorem real.cos_nonneg_of_mem_Icc {x : ℝ} :
-(π / 2) ≤ x → x ≤ π / 2 → 0 ≤ real.cos x

source
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} :
π / 2 < x → x < π + π / 2 → real.cos x < 0

source
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} :
π / 2 ≤ x → x ≤ π + π / 2 → real.cos x ≤ 0

source
theorem real.sin_nat_mul_pi (n : ℕ) :
real.sin ((↑n) * π) = 0

source
theorem real.sin_int_mul_pi (n : ℤ) :
real.sin ((↑n) * π) = 0

source
theorem real.cos_nat_mul_two_pi (n : ℕ) :
real.cos ((↑n) * 2 * π) = 1

source
theorem real.cos_int_mul_two_pi (n : ℤ) :
real.cos ((↑n) * 2 * π) = 1

source
theorem real.cos_int_mul_two_pi_add_pi (n : ℤ) :
real.cos ((↑n) * 2 * π + π) = -1

source
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : ℝ} :
-π < x → x < π → (real.sin x = 0 ↔ x = 0)

source
theorem real.sin_eq_zero_iff {x : ℝ} :
real.sin x = 0 ↔ ∃ (n : ℤ), (↑n) * π = 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 * π = x

source
theorem real.cos_eq_one_iff_of_lt_of_lt {x : ℝ} :
-2 * π < x → x < 2 * π → (real.cos x = 1 ↔ x = 0)

source
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : ℝ} :
0 ≤ x → y ≤ π / 2 → x < y → real.cos y < real.cos x

source
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} :
0 ≤ x → y ≤ π → x < y → real.cos y < real.cos x

source
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : ℝ} :
0 ≤ x → y ≤ π → x ≤ y → real.cos y ≤ real.cos x

source
theorem real.sin_lt_sin_of_le_of_le_pi_div_two {x y : ℝ} :
-(π / 2) ≤ x → y ≤ π / 2 → x < y → real.sin x < real.sin y

source
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} :
-(π / 2) ≤ x → y ≤ π / 2 → x ≤ y → real.sin x ≤ real.sin y

source
theorem real.sin_inj_of_le_of_le_pi_div_two {x y : ℝ} :
-(π / 2) ≤ x → x ≤ π / 2 → -(π / 2) ≤ y → y ≤ π / 2 → real.sin x = real.sin y → x = y

source
theorem real.cos_inj_of_nonneg_of_le_pi {x y : ℝ} :
0 ≤ x → x ≤ π → 0 ≤ y → y ≤ π → real.cos x = real.cos y → x = y

source
theorem real.exists_sin_eq  :
set.Icc (-1) 1 ⊆ real.sin '' set.Icc (-(π / 2)) (π / 2)

source
theorem real.exists_cos_eq  :
set.Icc (-1) 1 ⊆ real.cos '' set.Icc 0 π

source
theorem real.range_cos  :
set.range real.cos = set.Icc (-1) 1

source
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
theorem real.sin_lt {x : ℝ} :
0 < x → real.sin x < x

source
theorem real.sin_gt_sub_cube {x : ℝ} :
0 < x → x ≤ 1 → x - x ^ 3 / 4 < real.sin x

source
@[simp]
def real.sqrt_two_add_series  :
ℝ → ℕ → ℝ

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 : ℝ) :
x.sqrt_two_add_series 0 = x

source
theorem real.sqrt_two_add_series_one  :
0.sqrt_two_add_series 1 = real.sqrt 2

source
theorem real.sqrt_two_add_series_two  :
0.sqrt_two_add_series 2 = real.sqrt (2 + real.sqrt 2)

source
theorem real.sqrt_two_add_series_zero_nonneg (n : ℕ) :
0 ≤ 0.sqrt_two_add_series n

source
theorem real.sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) (n : ℕ) :
0 ≤ x.sqrt_two_add_series n

source
theorem real.sqrt_two_add_series_lt_two (n : ℕ) :
0.sqrt_two_add_series n < 2

source
theorem real.sqrt_two_add_series_succ (x : ℝ) (n : ℕ) :
x.sqrt_two_add_series (n + 1) = (real.sqrt (2 + x)).sqrt_two_add_series n

source
theorem real.sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) (n : ℕ) :
x.sqrt_two_add_series n ≤ y.sqrt_two_add_series n

source
@[simp]
theorem real.cos_pi_over_two_pow (n : ℕ) :
real.cos (π / 2 ^ (n + 1)) = 0.sqrt_two_add_series n / 2

source
theorem real.sin_square_pi_over_two_pow (n : ℕ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (0.sqrt_two_add_series n / 2) ^ 2

source
theorem real.sin_square_pi_over_two_pow_succ (n : ℕ) :
real.sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - 0.sqrt_two_add_series n / 4

source
@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ℕ) :
real.sin (π / 2 ^ (n + 2)) = real.sqrt (2 - 0.sqrt_two_add_series n) / 2

source
@[simp]
theorem real.cos_pi_div_four  :
real.cos (π / 4) = real.sqrt 2 / 2

source
@[simp]
theorem real.sin_pi_div_four  :
real.sin (π / 4) = real.sqrt 2 / 2

source
@[simp]
theorem real.cos_pi_div_eight  :
real.cos (π / 8) = real.sqrt (2 + real.sqrt 2) / 2

source
@[simp]
theorem real.sin_pi_div_eight  :
real.sin (π / 8) = real.sqrt (2 - real.sqrt 2) / 2

source
@[simp]
theorem real.cos_pi_div_sixteen  :
real.cos (π / 16) = real.sqrt (2 + real.sqrt (2 + real.sqrt 2)) / 2

source
@[simp]
theorem real.sin_pi_div_sixteen  :
real.sin (π / 16) = real.sqrt (2 - real.sqrt (2 + real.sqrt 2)) / 2

source
@[simp]
theorem real.cos_pi_div_thirty_two  :
real.cos (π / 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 (π / 32) = real.sqrt (2 - real.sqrt (2 + real.sqrt (2 + real.sqrt 2))) / 2

source
@[simp]
theorem real.cos_pi_div_three  :
real.cos (π / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

source
theorem real.square_cos_pi_div_six  :
real.cos (π / 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 (π / 6) = real.sqrt 3 / 2

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

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

The sine of π / 6 is 1 / 2.

source
theorem real.square_sin_pi_div_three  :
real.sin (π / 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 (π / 3) = real.sqrt 3 / 2

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

source
def real.angle  :
Type

The type of angles

Equations
source
@[instance]
def real.angle.angle.add_comm_group  :
add_comm_group real.angle

Equations
source
@[instance]
def real.angle.inhabited  :
inhabited real.angle

Equations
source
@[instance]
def real.angle.angle.has_coe  :
has_coe ℝ real.angle

Equations
source
@[simp]
theorem real.angle.coe_zero  :
↑0 = 0

source
@[simp]
theorem real.angle.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y

source
@[simp]
theorem real.angle.coe_neg (x : ℝ) :
↑-x = -↑x

source
@[simp]
theorem real.angle.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y

source
@[simp]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
↑(↑n) * x = n •ℕ ↑x

source
@[simp]
theorem real.angle.coe_int_mul_eq_gsmul (x : ℝ) (n : ℤ) :
↑(↑n) * x = n •ℤ ↑x

source
@[simp]
theorem real.angle.coe_two_pi  :
↑2 * π = 0

source
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} :
↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = (2 * π) * ↑k

source
theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : ℝ} :
real.cos θ = real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

source
theorem real.angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : ℝ} :
real.sin θ = real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

source
theorem real.angle.cos_sin_inj {θ ψ : ℝ} :
real.cos θ = real.cos ψ → real.sin θ = real.sin ψ → ↑θ = ↑ψ

source
def real.arcsin  :
ℝ → ℝ

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x and arcsin x ≤ π / 2. If the argument is not between -1 and 1 it defaults to 0

Equations
source
theorem real.arcsin_le_pi_div_two (x : ℝ) :
x.arcsin ≤ π / 2

source
theorem real.neg_pi_div_two_le_arcsin (x : ℝ) :
-(π / 2) ≤ x.arcsin

source
theorem real.sin_arcsin {x : ℝ} :
-1 ≤ x → x ≤ 1 → real.sin x.arcsin = x

source
theorem real.arcsin_sin {x : ℝ} :
-(π / 2) ≤ x → x ≤ π / 2 → (real.sin x).arcsin = x

source
theorem real.arcsin_inj {x y : ℝ} :
-1 ≤ x → x ≤ 1 → -1 ≤ y → y ≤ 1 → x.arcsin = y.arcsin → x = y

source
@[simp]
theorem real.arcsin_zero  :
0.arcsin = 0

source
@[simp]
theorem real.arcsin_one  :
1.arcsin = π / 2

source
@[simp]
theorem real.arcsin_neg (x : ℝ) :
(-x).arcsin = -x.arcsin

source
@[simp]
theorem real.arcsin_neg_one  :
(-1).arcsin = -(π / 2)

source
theorem real.arcsin_nonneg {x : ℝ} :
0 ≤ x → 0 ≤ x.arcsin

source
theorem real.arcsin_eq_zero_iff {x : ℝ} :
-1 ≤ x → x ≤ 1 → (x.arcsin = 0 ↔ x = 0)

source
theorem real.arcsin_pos {x : ℝ} :
0 < x → x ≤ 1 → 0 < x.arcsin

source
theorem real.arcsin_nonpos {x : ℝ} :
x ≤ 0 → x.arcsin ≤ 0

source
def real.arccos  :
ℝ → ℝ

Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. If the argument is not between -1 and 1 it defaults to π / 2

Equations
source
theorem real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) :
x.arccos = π / 2 - x.arcsin

source
theorem real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) :
x.arcsin = π / 2 - x.arccos

source
theorem real.arccos_le_pi (x : ℝ) :
x.arccos ≤ π

source
theorem real.arccos_nonneg (x : ℝ) :
0 ≤ x.arccos

source
theorem real.cos_arccos {x : ℝ} :
-1 ≤ x → x ≤ 1 → real.cos x.arccos = x

source
theorem real.arccos_cos {x : ℝ} :
0 ≤ x → x ≤ π → (real.cos x).arccos = x

source
theorem real.arccos_inj {x y : ℝ} :
-1 ≤ x → x ≤ 1 → -1 ≤ y → y ≤ 1 → x.arccos = y.arccos → x = y

source
@[simp]
theorem real.arccos_zero  :
0.arccos = π / 2

source
@[simp]
theorem real.arccos_one  :
1.arccos = 0

source
@[simp]
theorem real.arccos_neg_one  :
(-1).arccos = π

source
theorem real.arccos_neg (x : ℝ) :
(-x).arccos = π - x.arccos

source
theorem real.cos_arcsin_nonneg (x : ℝ) :
0 ≤ real.cos x.arcsin

source
theorem real.cos_arcsin {x : ℝ} :
-1 ≤ x → x ≤ 1 → real.cos x.arcsin = real.sqrt (1 - x ^ 2)

source
theorem real.sin_arccos {x : ℝ} :
-1 ≤ x → x ≤ 1 → real.sin x.arccos = real.sqrt (1 - x ^ 2)

source
theorem real.abs_div_sqrt_one_add_lt (x : ℝ) :
abs (x / real.sqrt (1 + x ^ 2)) < 1

source
theorem real.div_sqrt_one_add_lt_one (x : ℝ) :
x / real.sqrt (1 + x ^ 2) < 1

source
theorem real.neg_one_lt_div_sqrt_one_add (x : ℝ) :
-1 < x / real.sqrt (1 + x ^ 2)

source
@[simp]
theorem real.tan_pi_div_four  :
real.tan (π / 4) = 1

source
theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} :
0 < x → x < π / 2 → 0 < real.tan x

source
theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} :
0 ≤ x → x ≤ π / 2 → 0 ≤ real.tan x

source
theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} :
x < 0 → -(π / 2) < x → real.tan x < 0

source
theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} :
x ≤ 0 → -(π / 2) ≤ x → real.tan x ≤ 0

source
theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} :
0 ≤ x → y < π / 2 → x < y → real.tan x < real.tan y

source
theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : ℝ} :
-(π / 2) < x → y < π / 2 → x < y → real.tan x < real.tan y

source
theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : ℝ} :
-(π / 2) < x → x < π / 2 → -(π / 2) < y → y < π / 2 → real.tan x = real.tan y → x = y

source
def real.arctan  :
ℝ → ℝ

Inverse of the tan function, returns values in the range -π / 2 < arctan x and arctan x < π / 2

Equations
source
theorem real.sin_arctan (x : ℝ) :
real.sin x.arctan = x / real.sqrt (1 + x ^ 2)

source
theorem real.cos_arctan (x : ℝ) :
real.cos x.arctan = 1 / real.sqrt (1 + x ^ 2)

source
theorem real.tan_arctan (x : ℝ) :
real.tan x.arctan = x

source
theorem real.arctan_lt_pi_div_two (x : ℝ) :
x.arctan < π / 2

source
theorem real.neg_pi_div_two_lt_arctan (x : ℝ) :
-(π / 2) < x.arctan

source
theorem real.arctan_mem_Ioo (x : ℝ) :
x.arctan ∈ set.Ioo (-(π / 2)) (π / 2)

source
theorem real.tan_surjective  :
function.surjective real.tan

source
theorem real.arctan_tan {x : ℝ} :
-(π / 2) < x → x < π / 2 → (real.tan x).arctan = x

source
@[simp]
theorem real.arctan_zero  :
0.arctan = 0

source
@[simp]
theorem real.arctan_one  :
1.arctan = π / 4

source
@[simp]
theorem real.arctan_neg (x : ℝ) :
(-x).arctan = -x.arctan

source
def complex.arg  :
ℂ → ℝ

arg returns values in the range (-π, π], such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, arg 0 defaults to 0

Equations
source
theorem complex.arg_le_pi (x : ℂ) :
x.arg ≤ π

source
theorem complex.neg_pi_lt_arg (x : ℂ) :
-π < x.arg

source
theorem complex.arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg {x : ℂ} :
x.re < 0 → 0 ≤ x.im → x.arg = (-x).arg + π

source
theorem complex.arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg {x : ℂ} :
x.re < 0 → x.im < 0 → x.arg = (-x).arg - π

source
@[simp]
theorem complex.arg_zero  :
0.arg = 0

source
@[simp]
theorem complex.arg_one  :
1.arg = 0

source
@[simp]
theorem complex.arg_neg_one  :
(-1).arg = π

source
@[simp]
theorem complex.arg_I  :
complex.I.arg = π / 2

source
@[simp]
theorem complex.arg_neg_I  :
(-complex.I).arg = -(π / 2)

source
theorem complex.sin_arg (x : ℂ) :
real.sin x.arg = x.im / complex.abs x

source
theorem complex.cos_arg {x : ℂ} :
x ≠ 0 → real.cos x.arg = x.re / complex.abs x

source
theorem complex.tan_arg {x : ℂ} :
real.tan x.arg = x.im / x.re

source
theorem complex.arg_cos_add_sin_mul_I {x : ℝ} :
-π < x → x ≤ π → (complex.cos ↑x + (complex.sin ↑x) * complex.I).arg = x

source
theorem complex.arg_eq_arg_iff {x y : ℂ} :
x ≠ 0 → y ≠ 0 → (x.arg = y.arg ↔ (↑(complex.abs y) / ↑(complex.abs x)) * x = y)

source
theorem complex.arg_real_mul (x : ℂ) {r : ℝ} :
0 < r → ((↑r) * x).arg = x.arg

source
theorem complex.ext_abs_arg {x y : ℂ} :
complex.abs x = complex.abs y → x.arg = y.arg → x = y

source
theorem complex.arg_of_real_of_nonneg {x : ℝ} :
0 ≤ x → ↑x.arg = 0

source
theorem complex.arg_of_real_of_neg {x : ℝ} :
x < 0 → ↑x.arg = π

source
def complex.log  :
ℂ → ℂ

Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0

Equations
source
theorem complex.log_re (x : ℂ) :
x.log.re = real.log (complex.abs x)

source
theorem complex.log_im (x : ℂ) :
x.log.im = x.arg

source
theorem complex.exp_log {x : ℂ} :
x ≠ 0 → complex.exp x.log = x

source
theorem complex.range_exp  :
set.range complex.exp = {x : ℂ | x ≠ 0}

source
theorem complex.exp_inj_of_neg_pi_lt_of_le_pi {x y : ℂ} :
-π < x.im → x.im ≤ π → -π < y.im → y.im ≤ π → complex.exp x = complex.exp y → x = y

source
theorem complex.log_exp {x : ℂ} :
-π < x.im → x.im ≤ π → (complex.exp x).log = x

source
theorem complex.of_real_log {x : ℝ} :
0 ≤ x → ↑(real.log x) = ↑x.log

source
theorem complex.log_of_real_re (x : ℝ) :
↑x.log.re = real.log x

source
@[simp]
theorem complex.log_zero  :
0.log = 0

source
@[simp]
theorem complex.log_one  :
1.log = 0

source
theorem complex.log_neg_one  :
(-1).log = (↑π) * complex.I

source
theorem complex.log_I  :
complex.I.log = (↑π / 2) * complex.I

source
theorem complex.log_neg_I  :
(-complex.I).log = (-(↑π / 2)) * complex.I

source
theorem complex.exists_pow_nat_eq (x : ℂ) {n : ℕ} :
0 < n → (∃ (z : ℂ), z ^ n = x)

source
theorem complex.exists_eq_mul_self (x : ℂ) :
∃ (z : ℂ), x = z * z

source
theorem complex.two_pi_I_ne_zero  :
(2 * ↑π) * complex.I ≠ 0

source
theorem complex.exp_eq_one_iff {x : ℂ} :
complex.exp x = 1 ↔ ∃ (n : ℤ), x = (↑n) * (2 * ↑π) * complex.I

source
theorem complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} :
complex.exp x = complex.exp y ↔ complex.exp (x - y) = 1

source
theorem complex.exp_eq_exp_iff_exists_int {x y : ℂ} :
complex.exp x = complex.exp y ↔ ∃ (n : ℤ), x = y + (↑n) * (2 * ↑π) * complex.I

source
@[simp]
theorem complex.cos_pi_div_two  :
complex.cos (↑π / 2) = 0

source
@[simp]
theorem complex.sin_pi_div_two  :
complex.sin (↑π / 2) = 1

source
@[simp]
theorem complex.sin_pi  :
complex.sin ↑π = 0

source
@[simp]
theorem complex.cos_pi  :
complex.cos ↑π = -1

source
@[simp]
theorem complex.sin_two_pi  :
complex.sin (2 * ↑π) = 0

source
@[simp]
theorem complex.cos_two_pi  :
complex.cos (2 * ↑π) = 1

source
theorem complex.sin_add_pi (x : ℂ) :
complex.sin (x + ↑π) = -complex.sin x

source
theorem complex.sin_add_two_pi (x : ℂ) :
complex.sin (x + 2 * ↑π) = complex.sin x

source
theorem complex.cos_add_two_pi (x : ℂ) :
complex.cos (x + 2 * ↑π) = complex.cos x

source
theorem complex.sin_pi_sub (x : ℂ) :
complex.sin (↑π - x) = complex.sin x

source
theorem complex.cos_add_pi (x : ℂ) :
complex.cos (x + ↑π) = -complex.cos x

source
theorem complex.cos_pi_sub (x : ℂ) :
complex.cos (↑π - x) = -complex.cos x

source
theorem complex.sin_add_pi_div_two (x : ℂ) :
complex.sin (x + ↑π / 2) = complex.cos x

source
theorem complex.sin_sub_pi_div_two (x : ℂ) :
complex.sin (x - ↑π / 2) = -complex.cos x

source
theorem complex.sin_pi_div_two_sub (x : ℂ) :
complex.sin (↑π / 2 - x) = complex.cos x

source
theorem complex.cos_add_pi_div_two (x : ℂ) :
complex.cos (x + ↑π / 2) = -complex.sin x

source
theorem complex.cos_sub_pi_div_two (x : ℂ) :
complex.cos (x - ↑π / 2) = complex.sin x

source
theorem complex.cos_pi_div_two_sub (x : ℂ) :
complex.cos (↑π / 2 - x) = complex.sin x

source
theorem complex.sin_nat_mul_pi (n : ℕ) :
complex.sin ((↑n) * ↑π) = 0

source
theorem complex.sin_int_mul_pi (n : ℤ) :
complex.sin ((↑n) * ↑π) = 0

source
theorem complex.cos_nat_mul_two_pi (n : ℕ) :
complex.cos ((↑n) * 2 * ↑π) = 1

source
theorem complex.cos_int_mul_two_pi (n : ℤ) :
complex.cos ((↑n) * 2 * ↑π) = 1

source
theorem complex.cos_int_mul_two_pi_add_pi (n : ℤ) :
complex.cos ((↑n) * 2 * ↑π + ↑π) = -1

source
theorem complex.exp_pi_mul_I  :
complex.exp ((↑π) * complex.I) = -1

source
theorem complex.cos_eq_zero_iff {θ : ℂ} :
complex.cos θ = 0 ↔ ∃ (k : ℤ), θ = (2 * ↑k + 1) * ↑π / 2

source
theorem complex.cos_ne_zero_iff {θ : ℂ} :
complex.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑π / 2

source
theorem complex.sin_eq_zero_iff {θ : ℂ} :
complex.sin θ = 0 ↔ ∃ (k : ℤ), θ = (↑k) * ↑π

source
theorem complex.sin_ne_zero_iff {θ : ℂ} :
complex.sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (↑k) * ↑π

source
theorem complex.cos_eq_cos_iff {x y : ℂ} :
complex.cos x = complex.cos y ↔ ∃ (k : ℤ), y = (2 * ↑k) * ↑π + x ∨ y = (2 * ↑k) * ↑π - x

source
theorem complex.sin_eq_sin_iff {x y : ℂ} :
complex.sin x = complex.sin y ↔ ∃ (k : ℤ), y = (2 * ↑k) * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x

source
theorem complex.has_deriv_at_tan {x : ℂ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) → has_deriv_at complex.tan (1 / complex.cos x ^ 2) x

source
theorem complex.differentiable_at_tan {x : ℂ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) → differentiable_at ℂ complex.tan x

source
@[simp]
theorem complex.deriv_tan {x : ℂ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) → deriv complex.tan x = 1 / complex.cos x ^ 2

source
theorem complex.continuous_on_tan  :
continuous_on complex.tan {x : ℂ | complex.cos x ≠ 0}

source
theorem complex.continuous_tan  :
continuous (λ (x : ↥{x : ℂ | complex.cos x ≠ 0}), complex.tan ↑x)

source
theorem complex.cos_surjective  :
function.surjective complex.cos

source
@[simp]
theorem complex.range_cos  :
set.range complex.cos = set.univ

source
theorem complex.sin_surjective  :
function.surjective complex.sin

source
@[simp]
theorem complex.range_sin  :
set.range complex.sin = set.univ

source
theorem chebyshev₁_complex_cos (θ : ℂ) (n : ℕ) :
polynomial.eval (complex.cos θ) (polynomial.chebyshev₁ ℂ n) = complex.cos ((↑n) * θ)

the n-th Chebyshev polynomial evaluates on cos θ to the value cos (n * θ).

source
theorem cos_nat_mul (n : ℕ) (θ : ℂ) :
complex.cos ((↑n) * θ) = polynomial.eval (complex.cos θ) (polynomial.chebyshev₁ ℂ n)

cos (n * θ) is equal to the n-th Chebyshev polynomial evaluated on cos θ.

source
theorem real.cos_eq_zero_iff {θ : ℝ} :
real.cos θ = 0 ↔ ∃ (k : ℤ), θ = (2 * ↑k + 1) * π / 2

source
theorem real.cos_ne_zero_iff {θ : ℝ} :
real.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * π / 2

source
theorem real.cos_eq_cos_iff {x y : ℝ} :
real.cos x = real.cos y ↔ ∃ (k : ℤ), y = (2 * ↑k) * π + x ∨ y = (2 * ↑k) * π - x

source
theorem real.sin_eq_sin_iff {x y : ℝ} :
real.sin x = real.sin y ↔ ∃ (k : ℤ), y = (2 * ↑k) * π + x ∨ y = (2 * ↑k + 1) * π - x

source
theorem real.has_deriv_at_tan {x : ℝ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) → has_deriv_at real.tan (1 / real.cos x ^ 2) x

source
theorem real.differentiable_at_tan {x : ℝ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) → differentiable_at ℝ real.tan x

source
@[simp]
theorem real.deriv_tan {x : ℝ} :
(∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) → deriv real.tan x = 1 / real.cos x ^ 2

source
theorem real.continuous_tan  :
continuous (λ (x : ↥{x : ℝ | real.cos x ≠ 0}), real.tan ↑x)

source
theorem real.continuous_on_tan  :
continuous_on real.tan {x : ℝ | real.cos x ≠ 0}

source
theorem real.has_deriv_at_tan_of_mem_Ioo {x : ℝ} :
x ∈ set.Ioo (-(π / 2)) (π / 2) → has_deriv_at real.tan (1 / real.cos x ^ 2) x

source
theorem real.differentiable_at_tan_of_mem_Ioo {x : ℝ} :
x ∈ set.Ioo (-(π / 2)) (π / 2) → differentiable_at ℝ real.tan x

source
theorem real.deriv_tan_of_mem_Ioo {x : ℝ} :
x ∈ set.Ioo (-(π / 2)) (π / 2) → deriv real.tan x = 1 / real.cos x ^ 2

source
theorem real.continuous_on_tan_Ioo  :
continuous_on real.tan (set.Ioo (-(π / 2)) (π / 2))

source
theorem real.tendsto_sin_pi_div_two  :
filter.tendsto real.sin (𝓝[set.Iio (π / 2)] (π / 2)) (𝓝 1)

source
theorem real.tendsto_cos_pi_div_two  :
filter.tendsto real.cos (𝓝[set.Iio (π / 2)] (π / 2)) (𝓝[set.Ioi 0] 0)

source
theorem real.tendsto_tan_pi_div_two  :
filter.tendsto real.tan (𝓝[set.Iio (π / 2)] (π / 2)) filter.at_top

source
theorem real.tendsto_sin_neg_pi_div_two  :
filter.tendsto real.sin (𝓝[set.Ioi (-(π / 2))] -(π / 2)) (𝓝 (-1))

source
theorem real.tendsto_cos_neg_pi_div_two  :
filter.tendsto real.cos (𝓝[set.Ioi (-(π / 2))] -(π / 2)) (𝓝[set.Ioi 0] 0)

source
theorem real.tendsto_tan_neg_pi_div_two  :
filter.tendsto real.tan (𝓝[set.Ioi (-(π / 2))] -(π / 2)) filter.at_bot

Continuity and differentiability of arctan

The continuity of arctan is difficult to prove due to arctan being (indirectly) defined naively via classical.some. The proof therefore uses the general theorem that monotone functions are homeomorphisms: homeomorph_of_strict_mono_continuous_Ioo. We first prove that tan (restricted) is a homeomorphism whose inverse is definitionally equal to arctan. The fact that arctan is continuous is then derived from the fact that it is equal to a homeomorphism, and its differentiability is in turn derived from its continuity using has_deriv_at.of_local_left_inverse.

source
def real.tan_homeomorph  :
↥(set.Ioo (-(π / 2)) (π / 2)) ≃ₜ ℝ

The function tan, restricted to the open interval (-π/2, π/2), is a homeomorphism. The inverse function of that homeomorphism is definitionally equal to arctan via homeomorph.change_inv.

Equations
source
theorem real.tan_homeomorph_inv_fun_eq_arctan  :
coe ∘ real.tan_homeomorph.to_equiv.inv_fun = real.arctan

source
theorem real.continuous_arctan  :
continuous real.arctan

source
theorem real.has_deriv_at_arctan (x : ℝ) :
has_deriv_at real.arctan (1 / (1 + x ^ 2)) x

source
theorem real.differentiable_at_arctan (x : ℝ) :
differentiable_at ℝ real.arctan x

source
@[simp]
theorem real.deriv_arctan  :
deriv real.arctan = λ (x : ℝ), 1 / (1 + x ^ 2)

Register lemmas for the derivatives of the composition of real.arctan with a differentiable function, for standalone use and use with simp.

source
theorem has_deriv_at.arctan {f : ℝ → ℝ} {f' x : ℝ} :
has_deriv_at f f' x → has_deriv_at (λ (x : ℝ), (f x).arctan) ((1 / (1 + f x ^ 2)) * f') x

source
theorem has_deriv_within_at.arctan {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} :
has_deriv_within_at f f' s x → has_deriv_within_at (λ (x : ℝ), (f x).arctan) ((1 / (1 + f x ^ 2)) * f') s x

source
theorem differentiable_within_at.arctan {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → differentiable_within_at ℝ (λ (x : ℝ), (f x).arctan) s x

source
@[simp]
theorem differentiable_at.arctan {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), (f x).arctan) x

source
theorem differentiable_on.arctan {f : ℝ → ℝ} {s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), (f x).arctan) s

source
@[simp]
theorem differentiable.arctan {f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), (f x).arctan)

source
theorem deriv_within_arctan {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :
differentiable_within_at ℝ f s x → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), (f x).arctan) s x = (1 / (1 + f x ^ 2)) * deriv_within f s x

source
@[simp]
theorem deriv_arctan {f : ℝ → ℝ} {x : ℝ} :
differentiable_at ℝ f x → deriv (λ (x : ℝ), (f x).arctan) x = (1 / (1 + f x ^ 2)) * deriv f x