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.T_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 strictly differentiable, with the derivative cos x
.
The complex sine function is everywhere differentiable, with the derivative cos x
.
The complex cosine function is everywhere strictly differentiable, with the derivative
-sin x
.
The complex cosine function is everywhere differentiable, with the derivative -sin x
.
The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative
cosh x
.
The complex hyperbolic sine function is everywhere differentiable, with the derivative
cosh x
.
The complex hyperbolic cosine function is everywhere strictly differentiable, with the
derivative sinh 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 → ℂ
#
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