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)⁻¹.

`𝕂 = ℝ` or `𝕂 = ℂ` #

expSeries_radius_eq_top : the FormalMultilinearSeries defining exp 𝕂 has infinite radius of convergence
NormedSpace.exp_add_of_commute : given two commuting elements x and y, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
NormedSpace.exp_add : if 𝔸 is commutative, then we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y) for any x and y
NormedSpace.exp_neg : if 𝔸 is a division ring, then we have exp 𝕂 (-x) = (exp 𝕂 x)⁻¹.
exp_sum_of_commute : the analogous result to NormedSpace.exp_add_of_commute for Finset.sum.
exp_sum : the analogous result to NormedSpace.exp_add for Finset.sum.
NormedSpace.exp_nsmul : repeated addition in the domain corresponds to repeated multiplication in the codomain.
NormedSpace.exp_zsmul : repeated addition in the domain corresponds to repeated multiplication in the codomain.

Other useful compatibility results #

NormedSpace.exp_eq_exp : if 𝔸 is a normed algebra over two fields 𝕂 and 𝕂', then exp 𝕂 = exp 𝕂' 𝔸

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.