# 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} [] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (h : 0 < (NormedSpace.expSeries π πΈ).radius) :

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} [] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (h : 0 < (NormedSpace.expSeries π πΈ).radius) :

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} [] [NormedCommRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] [CharZero π] {x : πΈ} (hx : x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :

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} [] [NormedCommRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] [CharZero π] {x : πΈ} (hx : x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :

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} [] [CompleteSpace π] [CharZero π] {x : π} (hx : x β EMetric.ball 0 (NormedSpace.expSeries π π).radius) :

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} [] [CompleteSpace π] [CharZero π] {x : π} (hx : x β EMetric.ball 0 (NormedSpace.expSeries π π).radius) :
HasDerivAt (NormedSpace.exp π) (NormedSpace.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} [] [CompleteSpace π] (h : 0 < (NormedSpace.expSeries π π).radius) :

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} [] [CompleteSpace π] (h : 0 < (NormedSpace.expSeries π π).radius) :

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} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] :

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} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] :

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} [RCLike π] [NormedCommRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] {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} [RCLike π] [NormedCommRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] {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} [RCLike π] {x : π} :

The exponential map in π = β or π = β has strict derivative exp π x at any point x.

theorem hasDerivAt_exp {π : Type u_1} [RCLike π] {x : π} :
HasDerivAt (NormedSpace.exp π) (NormedSpace.exp π x) x

The exponential map in π = β or π = β has derivative exp π x at any point x.

theorem hasStrictDerivAt_exp_zero {π : Type u_1} [RCLike π] :

The exponential map in π = β or π = β has strict derivative 1 at zero.

theorem hasDerivAt_exp_zero {π : Type u_1} [RCLike π] :

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} [] [CharZero π] [NormedCommRing π] [NormedRing πΈ] [NormedSpace π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) β’ ) t
theorem hasFDerivAt_exp_smul_const_of_mem_ball' (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [] [CharZero π] [NormedCommRing π] [NormedRing πΈ] [NormedSpace π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (.smulRight (NormedSpace.exp π (t β’ x))) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [] [CharZero π] [NormedCommRing π] [NormedRing πΈ] [NormedSpace π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasStrictFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) β’ ) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [] [CharZero π] [NormedCommRing π] [NormedRing πΈ] [NormedSpace π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasStrictFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (.smulRight (NormedSpace.exp π (t β’ x))) t
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball {π : Type u_1} {πΈ : Type u_3} [] [CharZero π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasStrictDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) * x) t
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' {π : Type u_1} {πΈ : Type u_3} [] [CharZero π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasStrictDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (x * NormedSpace.exp π (t β’ x)) t
theorem hasDerivAt_exp_smul_const_of_mem_ball {π : Type u_1} {πΈ : Type u_3} [] [CharZero π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) * x) t
theorem hasDerivAt_exp_smul_const_of_mem_ball' {π : Type u_1} {πΈ : Type u_3} [] [CharZero π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) (htx : t β’ x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius) :
HasDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (x * NormedSpace.exp π (t β’ x)) t
theorem hasFDerivAt_exp_smul_const (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [RCLike π] [NormedCommRing π] [NormedRing πΈ] [NormedAlgebra π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) β’ ) t
theorem hasFDerivAt_exp_smul_const' (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [RCLike π] [NormedCommRing π] [NormedRing πΈ] [NormedAlgebra π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (.smulRight (NormedSpace.exp π (t β’ x))) t
theorem hasStrictFDerivAt_exp_smul_const (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [RCLike π] [NormedCommRing π] [NormedRing πΈ] [NormedAlgebra π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasStrictFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) β’ ) t
theorem hasStrictFDerivAt_exp_smul_const' (π : Type u_1) {π : Type u_2} {πΈ : Type u_3} [RCLike π] [NormedCommRing π] [NormedRing πΈ] [NormedAlgebra π π] [NormedAlgebra π πΈ] [Algebra π πΈ] [ContinuousSMul π πΈ] [IsScalarTower π π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasStrictFDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (.smulRight (NormedSpace.exp π (t β’ x))) t
theorem hasStrictDerivAt_exp_smul_const {π : Type u_1} {πΈ : Type u_3} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasStrictDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) * x) t
theorem hasStrictDerivAt_exp_smul_const' {π : Type u_1} {πΈ : Type u_3} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasStrictDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (x * NormedSpace.exp π (t β’ x)) t
theorem hasDerivAt_exp_smul_const {π : Type u_1} {πΈ : Type u_3} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (NormedSpace.exp π (t β’ x) * x) t
theorem hasDerivAt_exp_smul_const' {π : Type u_1} {πΈ : Type u_3} [RCLike π] [NormedRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] (x : πΈ) (t : π) :
HasDerivAt (fun (u : π) => NormedSpace.exp π (u β’ x)) (x * NormedSpace.exp π (t β’ x)) t
theorem HasSum.exp {π : Type u_1} {πΈ : Type u_2} [RCLike π] [NormedCommRing πΈ] [NormedAlgebra π πΈ] [CompleteSpace πΈ] {ΞΉ : Type u_3} {f : ΞΉ β πΈ} {a : πΈ} (h : HasSum f a) :
HasProd (NormedSpace.exp π β f) (NormedSpace.exp π a)

If f has sum a, then exp β f has product exp a.