Trigonometric functions
Main definitions
This file contains the following definitions:
- π, arcsin, arccos, arctan
- argument of a complex number
- logarithm on complex numbers
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
The complex sine function is everywhere differentiable, with the derivative cos x.
The complex cosine function is everywhere differentiable, with the derivative -sin x.
The complex hyperbolic sine function is everywhere differentiable, with the derivative sinh x.
The complex hyperbolic cosine function is everywhere differentiable, with the derivative cosh x.
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.
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
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
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
@[simp]
theorem
differentiable_at.ccos
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.cos (f x)) x
theorem
differentiable_on.ccos
{f : ℂ → ℂ}
{s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.cos (f x)) s
@[simp]
theorem
differentiable.ccos
{f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.cos (f x))
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
@[simp]
theorem
deriv_ccos
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.cos (f x)) x = -complex.sin (f x) * deriv f x
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
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
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
@[simp]
theorem
differentiable_at.csin
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.sin (f x)) x
theorem
differentiable_on.csin
{f : ℂ → ℂ}
{s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.sin (f x)) s
@[simp]
theorem
differentiable.csin
{f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.sin (f x))
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
@[simp]
theorem
deriv_csin
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.sin (f x)) x = complex.cos (f x) * deriv f x
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
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
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
@[simp]
theorem
differentiable_at.ccosh
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.cosh (f x)) x
theorem
differentiable_on.ccosh
{f : ℂ → ℂ}
{s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.cosh (f x)) s
@[simp]
theorem
differentiable.ccosh
{f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.cosh (f x))
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
@[simp]
theorem
deriv_ccosh
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.cosh (f x)) x = complex.sinh (f x) * deriv f x
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
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
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
@[simp]
theorem
differentiable_at.csinh
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → differentiable_at ℂ (λ (x : ℂ), complex.sinh (f x)) x
theorem
differentiable_on.csinh
{f : ℂ → ℂ}
{s : set ℂ} :
differentiable_on ℂ f s → differentiable_on ℂ (λ (x : ℂ), complex.sinh (f x)) s
@[simp]
theorem
differentiable.csinh
{f : ℂ → ℂ} :
differentiable ℂ f → differentiable ℂ (λ (x : ℂ), complex.sinh (f x))
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
@[simp]
theorem
deriv_csinh
{f : ℂ → ℂ}
{x : ℂ} :
differentiable_at ℂ f x → deriv (λ (x : ℂ), complex.sinh (f x)) x = complex.cosh (f x) * deriv f x
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.
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
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
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
@[simp]
theorem
differentiable_at.cos
{f : ℝ → ℝ}
{x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.cos (f x)) x
theorem
differentiable_on.cos
{f : ℝ → ℝ}
{s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.cos (f x)) s
@[simp]
theorem
differentiable.cos
{f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.cos (f x))
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
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
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
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
@[simp]
theorem
differentiable_at.sin
{f : ℝ → ℝ}
{x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.sin (f x)) x
theorem
differentiable_on.sin
{f : ℝ → ℝ}
{s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.sin (f x)) s
@[simp]
theorem
differentiable.sin
{f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.sin (f x))
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
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
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
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
@[simp]
theorem
differentiable_at.cosh
{f : ℝ → ℝ}
{x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.cosh (f x)) x
theorem
differentiable_on.cosh
{f : ℝ → ℝ}
{s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.cosh (f x)) s
@[simp]
theorem
differentiable.cosh
{f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.cosh (f x))
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
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
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
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
@[simp]
theorem
differentiable_at.sinh
{f : ℝ → ℝ}
{x : ℝ} :
differentiable_at ℝ f x → differentiable_at ℝ (λ (x : ℝ), real.sinh (f x)) x
theorem
differentiable_on.sinh
{f : ℝ → ℝ}
{s : set ℝ} :
differentiable_on ℝ f s → differentiable_on ℝ (λ (x : ℝ), real.sinh (f x)) s
@[simp]
theorem
differentiable.sinh
{f : ℝ → ℝ} :
differentiable ℝ f → differentiable ℝ (λ (x : ℝ), real.sinh (f x))
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
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
@[simp]
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
- x.sqrt_two_add_series (n + 1) = real.sqrt (2 + x.sqrt_two_add_series n)
- x.sqrt_two_add_series 0 = x
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
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
The type of angles
Equations
@[instance]
@[instance]
Equations
- real.angle.inhabited = {default := 0}
@[instance]
Equations
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
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
theorem
complex.exp_eq_exp_iff_exp_sub_eq_one
{x y : ℂ} :
complex.exp x = complex.exp y ↔ complex.exp (x - y) = 1