Exponential Function #
This file contains the definitions of the real and complex exponential function.
Main definitions #
Complex.exp
: The complex exponential function, defined via its Taylor seriesReal.exp
: The real exponential function, defined as the real part of the complex exponential
@[deprecated Complex.isCauSeq_norm_exp (since := "2025-02-16")]
Alias of Complex.isCauSeq_norm_exp
.
The complex exponential function, defined via its Taylor series
Equations
Instances For
scoped notation for the complex exponential function
Equations
Instances For
scoped notation for the real exponential function
Equations
Instances For
@[simp]
@[simp]
theorem
Complex.sum_div_factorial_le
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
(n j : ℕ)
(hn : 0 < n)
:
@[deprecated Complex.norm_exp_sub_sum_le_exp_norm_sub_sum (since := "2025-02-16")]
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
.
Equations
Instances For
@[deprecated Complex.norm_exp_ofReal (since := "2025-02-16")]
Alias of Complex.norm_exp_ofReal
.