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.
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 ⟶ ∞,