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_posfor the caseπΈ = π)has_strict_fderiv_at_exp_of_lt_radius: ifπhas characteristic zero andπΈis commutative, then given a pointxin the disk of convergence,exp πhas strict FrΓ©chet-derivativeexp π x β’ 1 : πΈ βL[π] πΈat x (see alsohas_strict_deriv_at_exp_of_lt_radiusfor 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 xattift β’ xis 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_zerofor 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_expfor 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 xatt.
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!