# Exponential in a Banach algebra #

In this file, we define exp 𝕂 : 𝔸 → 𝔸, the exponential map in a topological algebra 𝔸 over a field 𝕂.

While for most interesting results we need 𝔸 to be normed algebra, we do not require this in the definition in order to make exp independent of a particular choice of norm. The definition also does not require that 𝔸 be complete, but we need to assume it for most results.

We then prove some basic results, but we avoid importing derivatives here to minimize dependencies. Results involving derivatives and comparisons with Real.exp and Complex.exp can be found in Analysis.SpecialFunctions.Exponential.

## Main results #

We prove most result for an arbitrary field 𝕂, and then specialize to 𝕂 = ℝ or 𝕂 = ℂ.

### General case #

• NormedSpace.exp_add_of_commute_of_mem_ball : if 𝕂 has characteristic zero, then given two commuting elements x and y in the disk of convergence, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
• NormedSpace.exp_add_of_mem_ball : if 𝕂 has characteristic zero and 𝔸 is commutative, then given two elements x and y in the disk of convergence, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
• NormedSpace.exp_neg_of_mem_ball : if 𝕂 has characteristic zero and 𝔸 is a division ring, then given an element x in the disk of convergence, we have exp 𝕂 (-x) = (exp 𝕂 x)⁻¹.

### Notes #

We put nearly all the statements in this file in the NormedSpace namespace, to avoid collisions with the Real or Complex namespaces.

As of 2023-11-16 due to bad instances in Mathlib

import Mathlib

open Real

#time example (x : ℝ) : 0 < exp x      := exp_pos _ -- 250ms
#time example (x : ℝ) : 0 < Real.exp x := exp_pos _ -- 2ms

This is because exp x tries the NormedSpace.exp function defined here, and generates a slow coercion search from Real to Type, to fit the first argument here. We will resolve this slow coercion separately, but we want to move exp out of the root namespace in any case to avoid this ambiguity.

In the long term is may be possible to replace Real.exp and Complex.exp with this one.

def NormedSpace.expSeries (𝕂 : Type u_1) (𝔸 : Type u_2) [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] :

expSeries 𝕂 𝔸 is the FormalMultilinearSeries whose n-th term is the map (xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ. Its sum is the exponential map exp 𝕂 : 𝔸 → 𝔸.

Equations
Instances For
noncomputable def NormedSpace.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) :
𝔸

exp 𝕂 : 𝔸 → 𝔸 is the exponential map determined by the action of 𝕂 on 𝔸. It is defined as the sum of the FormalMultilinearSeries expSeries 𝕂 𝔸.

Note that when 𝔸 = Matrix n n 𝕂, this is the Matrix Exponential; see Analysis.NormedSpace.MatrixExponential for lemmas specific to that case.

Equations
Instances For
theorem NormedSpace.expSeries_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) (n : ) :
(() fun (x_1 : Fin n) => x) = (())⁻¹ x ^ n
theorem NormedSpace.expSeries_apply_eq' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) :
(fun (n : ) => () fun (x_1 : Fin n) => x) = fun (n : ) => (())⁻¹ x ^ n
theorem NormedSpace.expSeries_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) :
= ∑' (n : ), (())⁻¹ x ^ n
theorem NormedSpace.exp_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] :
= fun (x : 𝔸) => ∑' (n : ), (())⁻¹ x ^ n
theorem NormedSpace.expSeries_apply_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] (n : ) :
(() fun (x : Fin n) => 0) = Pi.single 0 1 n
@[simp]
theorem NormedSpace.exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] :
= 1
@[simp]
theorem NormedSpace.exp_op {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] (x : 𝔸) :
@[simp]
theorem NormedSpace.exp_unop {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] (x : 𝔸ᵐᵒᵖ) :
theorem NormedSpace.star_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] [] [] (x : 𝔸) :
theorem IsSelfAdjoint.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] [] [] {x : 𝔸} (h : ) :
theorem Commute.exp_right (𝕂 : Type u_1) {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] {x : 𝔸} {y : 𝔸} (h : Commute x y) :
Commute x ()
theorem Commute.exp_left (𝕂 : Type u_1) {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] {x : 𝔸} {y : 𝔸} (h : Commute x y) :
Commute () y
theorem Commute.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [Ring 𝔸] [Algebra 𝕂 𝔸] [] [] [] {x : 𝔸} {y : 𝔸} (h : Commute x y) :
Commute () ()
theorem NormedSpace.expSeries_apply_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) (n : ) :
(() fun (x_1 : Fin n) => x) = x ^ n / ()
theorem NormedSpace.expSeries_apply_eq_div' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) :
(fun (n : ) => () fun (x_1 : Fin n) => x) = fun (n : ) => x ^ n / ()
theorem NormedSpace.expSeries_sum_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [Algebra 𝕂 𝔸] [] [] (x : 𝔸) :
= ∑' (n : ), x ^ n / ()
theorem NormedSpace.exp_eq_tsum_div {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [Algebra 𝕂 𝔸] [] [] :
= fun (x : 𝔸) => ∑' (n : ), x ^ n / ()
theorem NormedSpace.norm_expSeries_summable_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => () fun (x_1 : Fin n) => x
theorem NormedSpace.norm_expSeries_summable_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => (())⁻¹ x ^ n
theorem NormedSpace.expSeries_summable_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => () fun (x_1 : Fin n) => x
theorem NormedSpace.expSeries_summable_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => (())⁻¹ x ^ n
theorem NormedSpace.expSeries_hasSum_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) (hx : ) :
HasSum (fun (n : ) => () fun (x_1 : Fin n) => x) ()
theorem NormedSpace.expSeries_hasSum_exp_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) (hx : ) :
HasSum (fun (n : ) => (())⁻¹ x ^ n) ()
theorem NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (h : ) :
theorem NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (h : ) :
theorem NormedSpace.continuousOn_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] :
theorem NormedSpace.analyticAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) (hx : ) :
theorem NormedSpace.exp_add_of_commute_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} {y : 𝔸} (hxy : Commute x y) (hx : ) (hy : ) :
NormedSpace.exp 𝕂 (x + y) = *

In a Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero, if x and y are in the disk of convergence and commute, then exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y).

noncomputable def NormedSpace.invertibleExpOfMemBall {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} (hx : ) :

exp 𝕂 x has explicit two-sided inverse exp 𝕂 (-x).

Equations
• = { invOf := NormedSpace.exp 𝕂 (-x), invOf_mul_self := , mul_invOf_self := }
Instances For
theorem NormedSpace.isUnit_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} (hx : ) :
theorem NormedSpace.invOf_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} (hx : ) [] :
theorem NormedSpace.map_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} {𝔹 : Type u_3} [] [] [] [] [] {F : Type u_4} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : ) (x : 𝔸) (hx : ) :
f () = NormedSpace.exp 𝕂 (f x)

Any continuous ring homomorphism commutes with exp.

theorem NormedSpace.algebraMap_exp_comm_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝕂) (hx : ) :
() () = NormedSpace.exp 𝕂 (() x)
theorem NormedSpace.norm_expSeries_div_summable_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => x ^ n / ()
theorem NormedSpace.expSeries_div_summable_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] (x : 𝔸) (hx : ) :
Summable fun (n : ) => x ^ n / ()
theorem NormedSpace.expSeries_div_hasSum_exp_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] (x : 𝔸) (hx : ) :
HasSum (fun (n : ) => x ^ n / ()) ()
theorem NormedSpace.exp_neg_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] {x : 𝔸} (hx : ) :
theorem NormedSpace.exp_add_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} {y : 𝔸} (hx : ) (hy : ) :
NormedSpace.exp 𝕂 (x + y) = *

In a commutative Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero, exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y) for all x, y in the disk of convergence.

theorem NormedSpace.expSeries_radius_eq_top (𝕂 : Type u_1) (𝔸 : Type u_2) [] [] [] :

In a normed algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, the series defining the exponential map has an infinite radius of convergence.

theorem NormedSpace.expSeries_radius_pos (𝕂 : Type u_1) (𝔸 : Type u_2) [] [] [] :
theorem NormedSpace.norm_expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) :
Summable fun (n : ) => () fun (x_1 : Fin n) => x
theorem NormedSpace.norm_expSeries_summable' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) :
Summable fun (n : ) => (())⁻¹ x ^ n
theorem NormedSpace.expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
Summable fun (n : ) => () fun (x_1 : Fin n) => x
theorem NormedSpace.expSeries_summable' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
Summable fun (n : ) => (())⁻¹ x ^ n
theorem NormedSpace.expSeries_hasSum_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
HasSum (fun (n : ) => () fun (x_1 : Fin n) => x) ()
theorem NormedSpace.exp_series_hasSum_exp' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
HasSum (fun (n : ) => (())⁻¹ x ^ n) ()
theorem NormedSpace.exp_hasFPowerSeriesOnBall {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] :
theorem NormedSpace.exp_hasFPowerSeriesAt_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] :
theorem NormedSpace.exp_continuous {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] :
theorem NormedSpace.exp_analytic {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
theorem NormedSpace.exp_add_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} {y : 𝔸} (hxy : Commute x y) :
NormedSpace.exp 𝕂 (x + y) = *

In a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, if x and y commute, then exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y).

noncomputable def NormedSpace.invertibleExp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :

exp 𝕂 x has explicit two-sided inverse exp 𝕂 (-x).

Equations
Instances For
theorem NormedSpace.isUnit_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
theorem NormedSpace.invOf_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) [] :
theorem Ring.inverse_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (x : 𝔸) :
theorem NormedSpace.exp_mem_unitary_of_mem_skewAdjoint (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] [] [] {x : 𝔸} (h : x ) :
theorem NormedSpace.exp_sum_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {ι : Type u_4} (s : ) (f : ι𝔸) (h : Set.Pairwise s fun (i j : ι) => Commute (f i) (f j)) :
NormedSpace.exp 𝕂 (Finset.sum s fun (i : ι) => f i) = Finset.noncommProd s (fun (i : ι) => NormedSpace.exp 𝕂 (f i))

In a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, if a family of elements f i mutually commute then exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i).

theorem NormedSpace.exp_nsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] (n : ) (x : 𝔸) :
NormedSpace.exp 𝕂 (n x) = ^ n
theorem NormedSpace.map_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [] [] [] [] [] [] {F : Type u_4} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : ) (x : 𝔸) :
f () = NormedSpace.exp 𝕂 (f x)

Any continuous ring homomorphism commutes with NormedSpace.exp.

theorem NormedSpace.exp_smul (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] {G : Type u_4} [] [] [] (g : G) (x : 𝔸) :
NormedSpace.exp 𝕂 (g x) = g
theorem NormedSpace.exp_units_conj (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (y : 𝔸ˣ) (x : 𝔸) :
NormedSpace.exp 𝕂 (y * x * y⁻¹) = y * * y⁻¹
theorem NormedSpace.exp_units_conj' (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] [] (y : 𝔸ˣ) (x : 𝔸) :
NormedSpace.exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * * y
@[simp]
theorem Prod.fst_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [] [] [] [] [] [] [] (x : 𝔸 × 𝔹) :
().1 = NormedSpace.exp 𝕂 x.1
@[simp]
theorem Prod.snd_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [] [] [] [] [] [] [] (x : 𝔸 × 𝔹) :
().2 = NormedSpace.exp 𝕂 x.2
@[simp]
theorem Pi.exp_apply (𝕂 : Type u_1) [] {ι : Type u_4} {𝔸 : ιType u_5} [] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (i : ι) :
= NormedSpace.exp 𝕂 (x i)
theorem Pi.exp_def (𝕂 : Type u_1) [] {ι : Type u_4} {𝔸 : ιType u_5} [] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) :
= fun (i : ι) => NormedSpace.exp 𝕂 (x i)
theorem Function.update_exp (𝕂 : Type u_1) [] {ι : Type u_4} {𝔸 : ιType u_5} [] [] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (j : ι) (xj : 𝔸 j) :
theorem NormedSpace.algebraMap_exp_comm {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝕂) :
() () = NormedSpace.exp 𝕂 (() x)
theorem NormedSpace.norm_expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] (x : 𝔸) :
Summable fun (n : ) => x ^ n / ()
theorem NormedSpace.expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] (x : 𝔸) :
Summable fun (n : ) => x ^ n / ()
theorem NormedSpace.expSeries_div_hasSum_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [] [] [] (x : 𝔸) :
HasSum (fun (n : ) => x ^ n / ()) ()
theorem NormedSpace.exp_neg {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (x : 𝔸) :
theorem NormedSpace.exp_zsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (z : ) (x : 𝔸) :
NormedSpace.exp 𝕂 (z x) = ^ z
theorem NormedSpace.exp_conj {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (y : 𝔸) (x : 𝔸) (hy : y 0) :
NormedSpace.exp 𝕂 (y * x * y⁻¹) = y * * y⁻¹
theorem NormedSpace.exp_conj' {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] (y : 𝔸) (x : 𝔸) (hy : y 0) :
NormedSpace.exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * * y
theorem NormedSpace.exp_add {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {x : 𝔸} {y : 𝔸} :
NormedSpace.exp 𝕂 (x + y) = *

In a commutative Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y).

theorem NormedSpace.exp_sum {𝕂 : Type u_1} {𝔸 : Type u_2} [] [] [] [] {ι : Type u_3} (s : ) (f : ι𝔸) :
NormedSpace.exp 𝕂 (Finset.sum s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => NormedSpace.exp 𝕂 (f i)

A version of NormedSpace.exp_sum_of_commute for a commutative Banach-algebra.

theorem NormedSpace.expSeries_eq_expSeries (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [] [Field 𝕂'] [Ring 𝔸] [Algebra 𝕂 𝔸] [Algebra 𝕂' 𝔸] [] [] (n : ) (x : 𝔸) :
(() fun (x_1 : Fin n) => x) = () fun (x_1 : Fin n) => x

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same expSeries on 𝔸.

theorem NormedSpace.exp_eq_exp (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [] [Field 𝕂'] [Ring 𝔸] [Algebra 𝕂 𝔸] [Algebra 𝕂' 𝔸] [] [] :

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same exponential function on 𝔸.

@[simp]
theorem NormedSpace.of_real_exp_ℝ_ℝ (r : ) :
() =

A version of Complex.ofReal_exp for NormedSpace.exp instead of Complex.exp