Complex and real exponential #
In this file we prove that Complex.exp
and Real.exp
are analytic functions.
Tags #
exp, derivative
The function Complex.exp
is complex analytic.
The function Complex.exp
is complex analytic.
The function Complex.exp
is complex analytic.
The function Complex.exp
is complex analytic.
exp ∘ f
is analytic
exp ∘ f
is analytic
exp ∘ f
is analytic
The complex exponential is everywhere differentiable, with the derivative exp x
.
The function Real.exp
is real analytic.
The function Real.exp
is real analytic.
The function Real.exp
is real analytic.
The function Real.exp
is real analytic.
exp ∘ f
is analytic
exp ∘ f
is analytic
exp ∘ f
is analytic
Register lemmas for the derivatives of the composition of Real.exp
with a differentiable
function, for standalone use and use with simp
.
Register lemmas for the derivatives of the composition of Real.exp
with a differentiable
function, for standalone use and use with simp
.