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 π
has strict FrΓ©chet-derivativeexp π x β’ 1 : πΈ βL[π] πΈ
at x (see alsohas_strict_deriv_at_exp_of_lt_radius
for the caseπΈ = π
)has_strict_fderiv_at_exp_smul_const_of_mem_ball
: even whenπΈ
is non-commutative, if we have an intermediate algebraπ
which is commutative, then the function(u : π) β¦ exp π (u β’ x)
, still has strict FrΓ©chet-derivativeexp π (t β’ x) β’ (1 : π βL[π] π).smul_right x
att
ift β’ x
is in the radius of convergence.
π = β
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 π
has strict FrΓ©chet-derivativeexp π x β’ 1 : πΈ βL[π] πΈ
at x (see alsohas_strict_deriv_at_exp
for the caseπΈ = π
)has_strict_fderiv_at_exp_smul_const
: even whenπΈ
is non-commutative, if we have an intermediate algebraπ
which is commutative, then the function(u : π) β¦ exp π (u β’ x)
still has strict FrΓ©chet-derivativeexp π (t β’ x) β’ (1 : πΈ βL[π] πΈ).smul_right x
att
.
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.
Derivative of $\exp (ux)$ by $u$ #
Note that since for x : πΈ
we have normed_ring πΈ
not normed_comm_ring πΈ
, we cannot deduce
these results from has_fderiv_at_exp_of_mem_ball
applied to the algebra πΈ
.
One possible solution for that would be to apply has_fderiv_at_exp_of_mem_ball
to the
commutative algebra algebra.elemental_algebra π x
. Unfortunately we don't have all the required
API, so we leave that to a future refactor (see leanprover-community/mathlib#19062 for discussion).
We could also go the other way around and deduce has_fderiv_at_exp_of_mem_ball
from
has_fderiv_at_exp_smul_const_of_mem_ball
applied to π := πΈ
, x := (1 : πΈ)
, and t := x
.
However, doing so would make the aformentioned elemental_algebra
refactor harder, so for now we
just prove these two lemmas independently.
A last strategy would be to deduce everything from the more general non-commutative case, $$\frac{d}{dt}e^{x(t)} = \int_0^1 e^{sx(t)} \left(\frac{d}{dt}e^{x(t)}\right) e^{(1-s)x(t)} ds$$ but this is harder to prove, and typically is shown by going via these results first.
TODO: prove this result too!