Calculus results on exponential in a Banach algebra #
In this file, we prove basic properties about the derivative of the exponential map exp π
in a Banach algebra πΈ
over a field π
. We keep them separate from the main file
analysis/normed_space/exponential
in order to minimize dependencies.
Main results #
We prove most result for an arbitrary field π
, and then specialize to π = β
or π = β
.
General case #
has_strict_fderiv_at_exp_zero_of_radius_pos
:exp π
has strict FrΓ©chet-derivative1 : πΈ βL[π] πΈ
at zero, as long as it converges on a neighborhood of zero (see alsohas_strict_deriv_at_exp_zero_of_radius_pos
for the caseπΈ = π
)has_strict_fderiv_at_exp_of_lt_radius
: ifπ
has characteristic zero andπΈ
is commutative, then given a pointx
in the disk of convergence,exp π
as strict FrΓ©chet-derivativeexp π x β’ 1 : πΈ βL[π] πΈ
at x (see alsohas_strict_deriv_at_exp_of_lt_radius
for the caseπΈ = π
)
π = β
or π = β
#
has_strict_fderiv_at_exp_zero
:exp π
has strict FrΓ©chet-derivative1 : πΈ βL[π] πΈ
at zero (see alsohas_strict_deriv_at_exp_zero
for the caseπΈ = π
)has_strict_fderiv_at_exp
: ifπΈ
is commutative, then given any pointx
,exp π
as strict FrΓ©chet-derivativeexp π x β’ 1 : πΈ βL[π] πΈ
at x (see alsohas_strict_deriv_at_exp
for the caseπΈ = π
)
Compatibilty with real.exp
and complex.exp
#
complex.exp_eq_exp_β
:complex.exp = exp β β
real.exp_eq_exp_β
:real.exp = exp β β
The exponential in a Banach-algebra πΈ
over a normed field π
has strict FrΓ©chet-derivative
1 : πΈ βL[π] πΈ
at zero, as long as it converges on a neighborhood of zero.
The exponential in a Banach-algebra πΈ
over a normed field π
has FrΓ©chet-derivative
1 : πΈ βL[π] πΈ
at zero, as long as it converges on a neighborhood of zero.
The exponential map in a commutative Banach-algebra πΈ
over a normed field π
of
characteristic zero has FrΓ©chet-derivative exp π x β’ 1 : πΈ βL[π] πΈ
at any point x
in the
disk of convergence.
The exponential map in a commutative Banach-algebra πΈ
over a normed field π
of
characteristic zero has strict FrΓ©chet-derivative exp π x β’ 1 : πΈ βL[π] πΈ
at any point x
in
the disk of convergence.
The exponential map in a complete normed field π
of characteristic zero has strict derivative
exp π x
at any point x
in the disk of convergence.
The exponential map in a complete normed field π
of characteristic zero has derivative
exp π x
at any point x
in the disk of convergence.
The exponential map in a complete normed field π
of characteristic zero has strict derivative
1
at zero, as long as it converges on a neighborhood of zero.
The exponential map in a complete normed field π
of characteristic zero has derivative
1
at zero, as long as it converges on a neighborhood of zero.
The exponential in a Banach-algebra πΈ
over π = β
or π = β
has strict FrΓ©chet-derivative
1 : πΈ βL[π] πΈ
at zero.
The exponential in a Banach-algebra πΈ
over π = β
or π = β
has FrΓ©chet-derivative
1 : πΈ βL[π] πΈ
at zero.
The exponential map in a commutative Banach-algebra πΈ
over π = β
or π = β
has strict
FrΓ©chet-derivative exp π x β’ 1 : πΈ βL[π] πΈ
at any point x
.
The exponential map in a commutative Banach-algebra πΈ
over π = β
or π = β
has
FrΓ©chet-derivative exp π x β’ 1 : πΈ βL[π] πΈ
at any point x
.
The exponential map in π = β
or π = β
has strict derivative exp π x
at any point
x
.
The exponential map in π = β
or π = β
has derivative exp π x
at any point x
.
The exponential map in π = β
or π = β
has strict derivative 1
at zero.
The exponential map in π = β
or π = β
has derivative 1
at zero.