# Documentation

Mathlib.Analysis.SpecialFunctions.Exponential

# 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 derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero, as long as it converges on a neighborhood of zero (see also hasStrictDerivAt_exp_zero_of_radius_pos for the case 𝔸 = 𝕂)
• hasStrictFDerivAt_exp_of_lt_radius : if 𝕂 has characteristic zero and 𝔸 is commutative, then given a point x in the disk of convergence, exp 𝕂 has strict Fréchet derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at x (see also hasStrictDerivAt_exp_of_lt_radius for 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 derivative exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x at t if t • x is in the radius of convergence.

### 𝕂 = ℝ or 𝕂 = ℂ#

• hasStrictFDerivAt_exp_zero : exp 𝕂 has strict Fréchet derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero (see also hasStrictDerivAt_exp_zero for the case 𝔸 = 𝕂)
• hasStrictFDerivAt_exp : if 𝔸 is commutative, then given any point x, exp 𝕂 has strict Fréchet derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at x (see also hasStrictDerivAt_exp for 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 derivative exp 𝕂 (t • x) • (1 : 𝔸 →L[𝕂] 𝔸).smulRight x at t.

### Compatibility with Real.exp and Complex.exp#

• Complex.exp_eq_exp_ℂ : Complex.exp = exp ℂ ℂ
• Real.exp_eq_exp_ℝ : Real.exp = exp ℝ ℝ
theorem hasStrictFDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (h : ) :

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.

theorem hasFDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (h : ) :
HasFDerivAt (exp 𝕂) 1 0

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.

theorem hasFDerivAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} (hx : x ) :
HasFDerivAt (exp 𝕂) (exp 𝕂 x 1) x

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.

theorem hasStrictFDerivAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} (hx : x ) :
HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x 1) x

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.

theorem hasStrictDerivAt_exp_of_mem_ball {𝕂 : Type u_1} [] [] {x : 𝕂} (hx : x ) :
HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x

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.

theorem hasDerivAt_exp_of_mem_ball {𝕂 : Type u_1} [] [] {x : 𝕂} (hx : x ) :
HasDerivAt (exp 𝕂) (exp 𝕂 x) x

The exponential map in a complete normed field 𝕂 of characteristic zero has derivative exp 𝕂 x at any point x in the disk of convergence.

theorem hasStrictDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} [] (h : ) :

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.

theorem hasDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} [] (h : ) :
HasDerivAt (exp 𝕂) 1 0

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.

theorem hasStrictFDerivAt_exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] :

The exponential in a Banach algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ has strict Fréchet derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero.

theorem hasFDerivAt_exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] :
HasFDerivAt (exp 𝕂) 1 0

The exponential in a Banach algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ has Fréchet derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero.

theorem hasStrictFDerivAt_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} :
HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x 1) x

The exponential map in a commutative Banach algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ has strict Fréchet derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at any point x.

theorem hasFDerivAt_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} :
HasFDerivAt (exp 𝕂) (exp 𝕂 x 1) x

The exponential map in a commutative Banach algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ has Fréchet derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at any point x.

theorem hasStrictDerivAt_exp {𝕂 : Type u_1} [] {x : 𝕂} :
HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x

The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has strict derivative exp 𝕂 x at any point x.

theorem hasDerivAt_exp {𝕂 : Type u_1} [] {x : 𝕂} :
HasDerivAt (exp 𝕂) (exp 𝕂 x) x

The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has derivative exp 𝕂 x at any point x.

theorem hasStrictDerivAt_exp_zero {𝕂 : Type u_1} [] :

The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has strict derivative 1 at zero.

theorem hasDerivAt_exp_zero {𝕂 : Type u_1} [] :
HasDerivAt (exp 𝕂) 1 0

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!

theorem hasFDerivAt_exp_smul_const_of_mem_ball (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) (htx : t x ) :
HasFDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) ) t
theorem hasFDerivAt_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) (htx : t x ) :
HasFDerivAt (fun u => exp 𝕂 (u x)) (ContinuousLinearMap.smulRight () (exp 𝕂 (t x))) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) (htx : t x ) :
HasStrictFDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) ) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) (htx : t x ) :
HasStrictFDerivAt (fun u => exp 𝕂 (u x)) (ContinuousLinearMap.smulRight () (exp 𝕂 (t x))) t
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) (htx : t x ) :
HasStrictDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) (htx : t x ) :
HasStrictDerivAt (fun u => exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem hasDerivAt_exp_smul_const_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) (htx : t x ) :
HasDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem hasDerivAt_exp_smul_const_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) (htx : t x ) :
HasDerivAt (fun u => exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem hasFDerivAt_exp_smul_const (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) :
HasFDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) ) t
theorem hasFDerivAt_exp_smul_const' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) :
HasFDerivAt (fun u => exp 𝕂 (u x)) (ContinuousLinearMap.smulRight () (exp 𝕂 (t x))) t
theorem hasStrictFDerivAt_exp_smul_const (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) :
HasStrictFDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) ) t
theorem hasStrictFDerivAt_exp_smul_const' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [] [] [] [] [] [Algebra 𝕊 𝔸] [] [] [] (x : 𝔸) (t : 𝕊) :
HasStrictFDerivAt (fun u => exp 𝕂 (u x)) (ContinuousLinearMap.smulRight () (exp 𝕂 (t x))) t
theorem hasStrictDerivAt_exp_smul_const {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) :
HasStrictDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem hasStrictDerivAt_exp_smul_const' {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) :
HasStrictDerivAt (fun u => exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem hasDerivAt_exp_smul_const {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) :
HasDerivAt (fun u => exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem hasDerivAt_exp_smul_const' {𝕂 : Type u_1} {𝔸 : Type u_3} [] [] [] [] (x : 𝔸) (t : 𝕂) :
HasDerivAt (fun u => exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t