Calculus results on exponential in a Banach algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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!