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/NormedSpace/Exponential in order to minimize dependencies.
Main results #
We prove most results for an arbitrary field π, and then specialize to π = β or π = β.
General case #
hasStrictFDerivAt_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 alsohasStrictDerivAt_exp_zero_of_radius_posfor the caseπΈ = π)hasStrictFDerivAt_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 alsohasStrictDerivAt_exp_of_lt_radiusfor the caseπΈ = π)hasStrictFDerivAt_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[π] π).smulRight xattift β’ xis in the radius of convergence.
π = β or π = β #
hasStrictFDerivAt_exp_zero:exp πhas strict FrΓ©chet derivative1 : πΈ βL[π] πΈat zero (see alsohasStrictDerivAt_exp_zerofor the caseπΈ = π)hasStrictFDerivAt_exp: ifπΈis commutative, then given any pointx,exp πhas strict FrΓ©chet derivativeexp π x β’ 1 : πΈ βL[π] πΈat x (see alsohasStrictDerivAt_expfor the caseπΈ = π)hasStrictFDerivAt_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[π] πΈ).smulRight xatt.
Compatibility 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 NormedRing πΈ not NormedCommRing πΈ, we cannot deduce
these results from hasFDerivAt_exp_of_mem_ball applied to the algebra πΈ.
One possible solution for that would be to apply hasFDerivAt_exp_of_mem_ball to the
commutative algebra Algebra.elementalAlgebra π 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 hasFDerivAt_exp_of_mem_ball from
hasFDerivAt_exp_smul_const_of_mem_ball applied to π := πΈ, x := (1 : πΈ), and t := x.
However, doing so would make the aforementioned elementalAlgebra 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!