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.Algebra.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:NormedSpace.exphas 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,NormedSpace.exphas strict Fréchet derivativeNormedSpace.exp 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, the function(u : 𝕊) ↦ NormedSpace.exp (u • x), still has strict Fréchet derivativeNormedSpace.exp (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight xattift • xis in the radius of convergence.
𝕂 = ℝ or 𝕂 = ℂ #
hasStrictFDerivAt_exp_zero:NormedSpace.exphas strict Fréchet derivative1 : 𝔸 →L[𝕂] 𝔸at zero (see alsohasStrictDerivAt_exp_zerofor the case𝔸 = 𝕂)hasStrictFDerivAt_exp: if𝔸is commutative, then given any pointx,NormedSpace.exphas strict Fréchet derivativeNormedSpace.exp 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, the function(u : 𝕊) ↦ NormedSpace.exp (u • x)still has strict Fréchet derivativeNormedSpace.exp (t • x) • (1 : 𝔸 →L[𝕂] 𝔸).smulRight xatt.
Compatibility with Real.exp and Complex.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 NormedSpace.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 NormedSpace.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
NormedSpace.exp x at any point x in the disk of convergence.
The exponential map in a complete normed field 𝕂 of characteristic zero has derivative
NormedSpace.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 NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸 at any point x.
The exponential map in a commutative Banach algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ has
Fréchet derivative NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸 at any point x.
The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has strict derivative NormedSpace.exp x
at any point x.
The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has derivative NormedSpace.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 https://github.com/leanprover-community/mathlib3/pull/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!
If f has sum a, then NormedSpace.exp ∘ f has product NormedSpace.exp a.