Exponential, trigonometric and hyperbolic trigonometric functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains the definitions of the real and complex exponential, sine, cosine, tangent, hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.
The Cauchy sequence consisting of partial sums of the Taylor series of the complex exponential function
The complex exponential function, defined via its Taylor series
- cexp z = (complex.exp' z).lim
The complex tangent function, defined as
sin z / cos z
- complex.tan z = complex.sin z / complex.cos z
The complex hyperbolic tangent function, defined as
sinh z / cosh z
- complex.tanh z = complex.sinh z / complex.cosh z
De Moivre's formula
This is an intermediate result that is later replaced by
real.add_one_le_exp; use that lemma
A finite initial segment of the exponential series, followed by an arbitrary tail.
n this is just a linear map wrt
r, and each map is a simple linear function
of the previous (see
exp_near n x r ⟶ exp x as
n ⟶ ∞,