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 elementsxandyin 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 elementsxandyin the disk of convergence, we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)
π = β or π = β #
exp_series_radius_eq_top: theformal_multilinear_seriesdefiningexp π πΈhas infinite radius of convergenceexp_add_of_commute: given two commuting elementsxandy, we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)exp_add: ifπΈis commutative, then we haveexp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y)for anyxandy
Other useful compatibility results #
exp_eq_exp: ifπΈis a normed algebra over two fieldsπandπ', thenexp π πΈ = exp π' πΈ
def
exp_series
(π : Type u_1)
(πΈ : Type u_2)
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ] :
formal_multilinear_series π πΈ πΈ
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 πΈ
noncomputable
def
exp
(π : Type u_1)
(πΈ : Type u_2)
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
πΈ
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
theorem
exp_series_apply_eq
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ)
(n : β) :
theorem
exp_series_apply_eq'
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
theorem
exp_series_apply_eq_field
{π : Type u_1}
[nondiscrete_normed_field π]
(x : π)
(n : β) :
theorem
exp_series_sum_eq
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
theorem
exp_eq_tsum
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ] :
theorem
exp_zero
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ] :
theorem
norm_exp_series_summable_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
norm_exp_series_summable_of_mem_ball'
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
norm_exp_series_field_summable_of_mem_ball
{π : Type u_1}
[nondiscrete_normed_field π]
(x : π)
(hx : x β emetric.ball 0 (exp_series π π).radius) :
theorem
exp_series_summable_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
summable (Ξ» (n : β), β(exp_series π πΈ n) (Ξ» (_x : fin n), x))
theorem
exp_series_summable_of_mem_ball'
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_field_summable_of_mem_ball
{π : Type u_1}
[nondiscrete_normed_field π]
[complete_space π]
(x : π)
(hx : x β emetric.ball 0 (exp_series π π).radius) :
theorem
exp_series_has_sum_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_has_sum_exp_of_mem_ball'
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_field_has_sum_exp_of_mem_ball
{π : Type u_1}
[nondiscrete_normed_field π]
[complete_space π]
(x : π)
(hx : x β emetric.ball 0 (exp_series π π).radius) :
theorem
has_fpower_series_on_ball_exp_of_radius_pos
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(h : 0 < (exp_series π πΈ).radius) :
has_fpower_series_on_ball (exp π πΈ) (exp_series π πΈ) 0 (exp_series π πΈ).radius
theorem
has_fpower_series_at_exp_zero_of_radius_pos
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(h : 0 < (exp_series π πΈ).radius) :
has_fpower_series_at (exp π πΈ) (exp_series π πΈ) 0
theorem
continuous_on_exp
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ] :
continuous_on (exp π πΈ) (emetric.ball 0 (exp_series π πΈ).radius)
theorem
analytic_at_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
analytic_at π (exp π πΈ) x
theorem
exp_add_of_commute_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[char_zero π]
{x y : πΈ}
(hxy : commute x y)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius)
(hy : y β emetric.ball 0 (exp_series π πΈ).radius) :
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).
theorem
exp_add_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nondiscrete_normed_field π]
[normed_comm_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[char_zero π]
{x y : πΈ}
(hx : x β emetric.ball 0 (exp_series π πΈ).radius)
(hy : y β emetric.ball 0 (exp_series π πΈ).radius) :
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
exp_series_radius_eq_top
(π : Type u_1)
(πΈ : Type u_2)
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ] :
(exp_series π πΈ).radius = β€
In a normed algebra πΈ over π = β or π = β, the series defining the exponential map
has an infinite radius of convergence.
theorem
exp_series_radius_pos
(π : Type u_1)
(πΈ : Type u_2)
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ] :
0 < (exp_series π πΈ).radius
theorem
norm_exp_series_summable
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
theorem
norm_exp_series_summable'
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
theorem
exp_series_summable
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
summable (Ξ» (n : β), β(exp_series π πΈ n) (Ξ» (_x : fin n), x))
theorem
exp_series_summable'
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_series_has_sum_exp
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_series_has_sum_exp'
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_has_fpower_series_on_ball
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ] :
has_fpower_series_on_ball (exp π πΈ) (exp_series π πΈ) 0 β€
theorem
exp_has_fpower_series_at_zero
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ] :
has_fpower_series_at (exp π πΈ) (exp_series π πΈ) 0
theorem
exp_continuous
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ] :
continuous (exp π πΈ)
theorem
exp_analytic
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
analytic_at π (exp π πΈ) x
theorem
exp_add_of_commute
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
{x y : πΈ}
(hxy : commute x y) :
In a Banach-algebra πΈ over π = β or π = β, if x and y commute, then
exp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y).
theorem
exp_add
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_comm_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
{x y : πΈ} :
In a commutative Banach-algebra πΈ over π = β or π = β,
exp π πΈ (x+y) = (exp π πΈ x) * (exp π πΈ y).
theorem
exp_series_eq_exp_series
(π : Type u_1)
(π' : Type u_2)
(πΈ : Type u_3)
[nondiscrete_normed_field π]
[nondiscrete_normed_field π']
[normed_ring πΈ]
[normed_algebra π πΈ]
[normed_algebra π' πΈ]
(n : β)
(x : πΈ) :
β(exp_series π πΈ n) (Ξ» (_x : fin n), x) = β(exp_series π' πΈ n) (Ξ» (_x : fin n), x)
If a normed ring πΈ is a normed algebra over two fields, then they define the same
exp_series on πΈ.
theorem
exp_eq_exp
(π : Type u_1)
(π' : Type u_2)
(πΈ : Type u_3)
[nondiscrete_normed_field π]
[nondiscrete_normed_field π']
[normed_ring πΈ]
[normed_algebra π πΈ]
[normed_algebra π' πΈ] :
If a normed ring πΈ is a normed algebra over two fields, then they define the same
exponential function on πΈ.