Exponential in a Banach algebra #
In this file, we define exp π πΈ
, the exponential map in a normed algebra πΈ
over a nondiscrete
normed field π
. Although the definition doesn't require πΈ
to be complete, 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/special_functions/exponential
.
Main results #
We prove most result for an arbitrary field π
, and then specialize to π = β
or π = β
.
General case #
exp_add_of_commute_of_lt_radius
: ifπ
has characteristic zero, then given two commuting elementsx
andy
in the disk of convergence, we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
exp_add_of_lt_radius
: ifπ
has characteristic zero andπΈ
is commutative, then given two elementsx
andy
in the disk of convergence, we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
π = β
or π = β
#
exp_series_radius_eq_top
: theformal_multilinear_series
definingexp π πΈ
has infinite radius of convergenceexp_add_of_commute
: given two commuting elementsx
andy
, we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
exp_add
: ifπΈ
is commutative, then we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
for anyx
andy
Other useful compatibility results #
exp_eq_exp
: ifπΈ
is a normed algebra over two fieldsπ
andπ'
, thenexp π πΈ = exp π' πΈ
In a Banach algebra πΈ
over a normed field π
, exp_series π πΈ
is the
formal_multilinear_series
whose n
-th term is the map (xα΅’) : πΈβΏ β¦ (1/n! : π) β’ β xα΅’
.
Its sum is the exponential map exp π πΈ : πΈ β πΈ
.
Equations
- exp_series π πΈ = Ξ» (n : β), (1 / βn!) β’ continuous_multilinear_map.mk_pi_algebra_fin π n πΈ
In a Banach algebra πΈ
over a normed field π
, exp π πΈ : πΈ β πΈ
is the exponential map
determined by the action of π
on πΈ
.
It is defined as the sum of the formal_multilinear_series
exp_series π πΈ
.
Equations
- exp π πΈ x = (exp_series π πΈ).sum x
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)
.
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.
In a normed algebra πΈ
over π = β
or π = β
, the series defining the exponential map
has an infinite radius of convergence.
In a Banach-algebra πΈ
over π = β
or π = β
, if x
and y
commute, then
exp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
.
In a commutative Banach-algebra πΈ
over π = β
or π = β
,
exp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
.
If a normed ring πΈ
is a normed algebra over two fields, then they define the same
exp_series
on πΈ
.
If a normed ring πΈ
is a normed algebra over two fields, then they define the same
exponential function on πΈ
.