Trigonometric functions #
Main definitions #
This file contains the definition of
analysis.special_functions.trigonometric.arctan for the inverse trigonometric functions.
analysis.special_functions.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
as they are most easily proved by appealing to the corresponding fact for
complex trigonometric functions.
analysis.special_functions.trigonometric.chebyshev for the multiple angle formulas
in terms of Chebyshev polynomials.
sin, cos, tan, angle
sqrt_two_add_series x n is
sqrt(2 + sqrt(2 + ... )) with
n square roots,
x. We define it here because
cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2