Exponential, trigonometric and hyperbolic trigonometric functions #
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
Instances For
The complex exponential function, defined via its Taylor series
Instances For
The complex hyperbolic cosine function, defined via exp
Instances For
scoped notation for the complex exponential function
Instances For
scoped notation for the real exponential function
Instances For
the exponential function as a monoid hom from Multiplicative ℂ
to ℂ
Instances For
De Moivre's formula
the exponential function as a monoid hom from Multiplicative ℝ
to ℝ
Instances For
This is an intermediate result that is later replaced by Real.add_one_le_exp
; use that lemma
instead.
A finite initial segment of the exponential series, followed by an arbitrary tail.
For fixed n
this is just a linear map wrt r
, and each map is a simple linear function
of the previous (see expNear_succ
), with expNear n x r ⟶ exp x
as n ⟶ ∞
,
for any r
.
Instances For
Extension for the positivity
tactic: Real.exp
is always positive.