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.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 #

𝕂 = ℝ or 𝕂 = β„‚ #

Compatibility with Real.exp and Complex.exp #

theorem hasStrictFDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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 NormedSpace.exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point xin the disk of convergence.

theorem hasStrictFDerivAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [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 NormedSpace.exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x in the disk of convergence.

theorem hasStrictDerivAt_exp_of_mem_ball {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] [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 NormedSpace.exp 𝕂 x at any point x in the disk of convergence.

theorem hasDerivAt_exp_of_mem_ball {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] [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 NormedSpace.exp 𝕂 x at any point x in the disk of convergence.

theorem hasStrictDerivAt_exp_zero_of_radius_pos {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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 NormedSpace.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 NormedSpace.exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x.

theorem hasStrictDerivAt_exp {𝕂 : Type u_1} [RCLike 𝕂] {x : 𝕂} :

The exponential map in 𝕂 = ℝ or 𝕂 = β„‚ has strict derivative NormedSpace.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 NormedSpace.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} [NontriviallyNormedField 𝕂] [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) β€’ ContinuousLinearMap.smulRight 1 x) t
theorem hasFDerivAt_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {π•Š : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [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)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t β€’ x))) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (𝕂 : Type u_1) {π•Š : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [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) β€’ ContinuousLinearMap.smulRight 1 x) t
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {π•Š : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [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)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t β€’ x))) t
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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} [NontriviallyNormedField 𝕂] [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) β€’ ContinuousLinearMap.smulRight 1 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)) ((ContinuousLinearMap.smulRight 1 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) β€’ ContinuousLinearMap.smulRight 1 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)) ((ContinuousLinearMap.smulRight 1 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 NormedSpace.exp ∘ f has product NormedSpace.exp a.