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.
polynomial.chebyshev₁_complex_cos
: then
-th Chebyshev polynomial evaluates oncomplex.cos θ
to the valuen * complex.cos θ
.
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
cosh x
.
The complex hyperbolic cosine function is everywhere differentiable, with the derivative
sinh x
.
Simp lemmas for derivatives of λ x, complex.cos (f x)
etc., f : ℂ → ℂ
Simp lemmas for derivatives of λ x, complex.cos (f x)
etc., f : E → ℂ
Simp lemmas for derivatives of λ x, real.cos (f x)
etc., f : ℝ → ℝ
Simp lemmas for derivatives of λ x, real.cos (f x)
etc., f : E → ℝ
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
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
- real.sqrt_two_add_series x (n + 1) = real.sqrt (2 + real.sqrt_two_add_series x n)
- real.sqrt_two_add_series x 0 = x
The type of angles
Equations
Equations
- real.angle.inhabited = {default := 0}
Equations
Inverse of the sin
function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2
.
It defaults to -π / 2
on (-∞, -1)
and to π / 2
to (1, ∞)
.
Equations
- real.arcsin = coe ∘ set.Icc_extend real.arcsin._proof_1 ⇑(real.sin_order_iso.symm)
real.sin
as a local_homeomorph
between (-π / 2, π / 2)
and (-1, 1)
.
Equations
- real.sin_local_homeomorph = {to_local_equiv := {to_fun := real.sin, inv_fun := real.arcsin, source := set.Ioo (-(π / 2)) (π / 2), target := set.Ioo (-1) 1, map_source' := real.maps_to_sin_Ioo, map_target' := real.sin_local_homeomorph._proof_1, left_inv' := real.sin_local_homeomorph._proof_2, right_inv' := real.sin_local_homeomorph._proof_3}, open_source := real.sin_local_homeomorph._proof_4, open_target := real.sin_local_homeomorph._proof_5, continuous_to_fun := real.sin_local_homeomorph._proof_6, continuous_inv_fun := real.sin_local_homeomorph._proof_7}
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
- real.arccos x = π / 2 - real.arcsin x
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
- x.arg = ite (0 ≤ x.re) (real.arcsin (x.im / complex.abs x)) (ite (0 ≤ x.im) (real.arcsin ((-x).im / complex.abs x) + π) (real.arcsin ((-x).im / complex.abs x) - π))
Inverse of the exp
function. Returns values such that (log x).im > - π
and (log x).im ≤ π
.
log 0 = 0
Equations
- complex.log x = ↑(