Exponential in a Banach algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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/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_mem_ball: ifπhas characteristic zero, then given two commuting elementsxandyin the disk of convergence, we haveexp π (x+y) = (exp π x) * (exp π y)exp_add_of_mem_ball: ifπhas characteristic zero andπΈis commutative, then given two elementsxandyin the disk of convergence, we haveexp π (x+y) = (exp π x) * (exp π y)exp_neg_of_mem_ball: ifπhas characteristic zero andπΈis a division ring, then given an elementxin the disk of convergence, we haveexp π (-x) = (exp π x)β»ΒΉ.
π = β 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 anyxandyexp_neg: ifπΈis a division ring, then we haveexp π (-x) = (exp π x)β»ΒΉ.exp_sum_of_commute: the analogous result toexp_add_of_commuteforfinset.sum.exp_sum: the analogous result toexp_addforfinset.sum.exp_nsmul: repeated addition in the domain corresponds to repeated multiplication in the codomain.exp_zsmul: repeated addition in the domain corresponds to repeated multiplication in the codomain.
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)
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ] :
formal_multilinear_series π πΈ πΈ
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 : β), (β(n.factorial))β»ΒΉ β’ continuous_multilinear_map.mk_pi_algebra_fin π n πΈ
noncomputable
def
exp
(π : Type u_1)
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ) :
πΈ
exp π : πΈ β πΈ is the exponential map determined by the action of π on πΈ.
It is defined as the sum of the formal_multilinear_series exp_series π πΈ.
Note that when πΈ = matrix n n π, this is the Matrix Exponential; see
analysis.normed_space.matrix_exponential for lemmas specific to that
case.
Equations
- exp π x = (exp_series π πΈ).sum x
theorem
exp_series_apply_eq
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ)
(n : β) :
theorem
exp_series_apply_eq'
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ) :
theorem
exp_series_sum_eq
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ) :
theorem
exp_series_apply_zero
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(n : β) :
β(exp_series π πΈ n) (Ξ» (_x : fin n), 0) = pi.single 0 1 n
@[simp]
theorem
exp_op
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
(x : πΈ) :
exp π (mul_opposite.op x) = mul_opposite.op (exp π x)
@[simp]
theorem
exp_unop
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
(x : πΈα΅α΅α΅) :
exp π (mul_opposite.unop x) = mul_opposite.unop (exp π x)
theorem
star_exp
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
[star_ring πΈ]
[has_continuous_star πΈ]
(x : πΈ) :
has_star.star (exp π x) = exp π (has_star.star x)
theorem
is_self_adjoint.exp
(π : Type u_1)
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
[star_ring πΈ]
[has_continuous_star πΈ]
{x : πΈ}
(h : is_self_adjoint x) :
is_self_adjoint (exp π x)
theorem
commute.exp_right
(π : Type u_1)
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
{x y : πΈ}
(h : commute x y) :
theorem
commute.exp_left
(π : Type u_1)
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
{x y : πΈ}
(h : commute x y) :
theorem
commute.exp
(π : Type u_1)
{πΈ : Type u_2}
[field π]
[ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
[t2_space πΈ]
{x y : πΈ}
(h : commute x y) :
theorem
exp_series_apply_eq_div
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[division_ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ)
(n : β) :
theorem
exp_series_apply_eq_div'
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[division_ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ) :
theorem
exp_series_sum_eq_div
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[division_ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(x : πΈ) :
theorem
exp_eq_tsum_div
{π : Type u_1}
{πΈ : Type u_2}
[field π]
[division_ring πΈ]
[algebra π πΈ]
[topological_space πΈ]
[topological_ring πΈ] :
theorem
norm_exp_series_summable_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_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}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_summable_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_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}
[nontrivially_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}
[nontrivially_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}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[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}
[nontrivially_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}
[nontrivially_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}
[nontrivially_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}
[nontrivially_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}
[nontrivially_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).
noncomputable
def
invertible_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[char_zero π]
{x : πΈ}
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
invertible (exp π x)
exp π x has explicit two-sided inverse exp π (-x).
Equations
- invertible_exp_of_mem_ball hx = {inv_of := exp π (-x), inv_of_mul_self := _, mul_inv_of_self := _}
theorem
is_unit_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[char_zero π]
{x : πΈ}
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
inv_of_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[char_zero π]
{x : πΈ}
(hx : x β emetric.ball 0 (exp_series π πΈ).radius)
[invertible (exp π x)] :
theorem
map_exp_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
{πΉ : Type u_3}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_ring πΉ]
[normed_algebra π πΈ]
[normed_algebra π πΉ]
[complete_space πΈ]
{F : Type u_4}
[ring_hom_class F πΈ πΉ]
(f : F)
(hf : continuous βf)
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
Any continuous ring homomorphism commutes with exp.
theorem
algebra_map_exp_comm_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space π]
(x : π)
(hx : x β emetric.ball 0 (exp_series π π).radius) :
β(algebra_map π πΈ) (exp π x) = exp π (β(algebra_map π πΈ) x)
theorem
norm_exp_series_div_summable_of_mem_ball
(π : Type u_1)
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_div_summable_of_mem_ball
(π : Type u_1)
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_series_div_has_sum_exp_of_mem_ball
(π : Type u_1)
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_neg_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_normed_field π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[char_zero π]
[complete_space πΈ]
{x : πΈ}
(hx : x β emetric.ball 0 (exp_series π πΈ).radius) :
theorem
exp_add_of_mem_ball
{π : Type u_1}
{πΈ : Type u_2}
[nontrivially_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
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
@[continuity]
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).
noncomputable
def
invertible_exp
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
invertible (exp π x)
exp π x has explicit two-sided inverse exp π (-x).
Equations
- invertible_exp π x = invertible_exp_of_mem_ball _
theorem
is_unit_exp
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
inv_of_exp
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ)
[invertible (exp π x)] :
theorem
ring.inverse_exp
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
ring.inverse (exp π x) = exp π (-x)
theorem
exp_mem_unitary_of_mem_skew_adjoint
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
[star_ring πΈ]
[has_continuous_star πΈ]
{x : πΈ}
(h : x β skew_adjoint πΈ) :
theorem
exp_sum_of_commute
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
{ΞΉ : Type u_3}
(s : finset ΞΉ)
(f : ΞΉ β πΈ)
(h : βs.pairwise (Ξ» (i j : ΞΉ), commute (f i) (f j))) :
exp π (s.sum (Ξ» (i : ΞΉ), f i)) = s.noncomm_prod (Ξ» (i : ΞΉ), 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
exp_nsmul
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(n : β)
(x : πΈ) :
theorem
map_exp
(π : Type u_1)
{πΈ : Type u_2}
{πΉ : Type u_3}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[normed_ring πΉ]
[normed_algebra π πΉ]
[complete_space πΈ]
{F : Type u_4}
[ring_hom_class F πΈ πΉ]
(f : F)
(hf : continuous βf)
(x : πΈ) :
Any continuous ring homomorphism commutes with exp.
theorem
exp_smul
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
{G : Type u_3}
[monoid G]
[mul_semiring_action G πΈ]
[has_continuous_const_smul G πΈ]
(g : G)
(x : πΈ) :
@[simp]
theorem
prod.fst_exp
(π : Type u_1)
{πΈ : Type u_2}
{πΉ : Type u_3}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[normed_ring πΉ]
[normed_algebra π πΉ]
[complete_space πΈ]
[complete_space πΉ]
(x : πΈ Γ πΉ) :
@[simp]
theorem
prod.snd_exp
(π : Type u_1)
{πΈ : Type u_2}
{πΉ : Type u_3}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
[normed_ring πΉ]
[normed_algebra π πΉ]
[complete_space πΈ]
[complete_space πΉ]
(x : πΈ Γ πΉ) :
@[simp]
theorem
pi.exp_apply
(π : Type u_1)
[is_R_or_C π]
{ΞΉ : Type u_2}
{πΈ : ΞΉ β Type u_3}
[fintype ΞΉ]
[Ξ (i : ΞΉ), normed_ring (πΈ i)]
[Ξ (i : ΞΉ), normed_algebra π (πΈ i)]
[β (i : ΞΉ), complete_space (πΈ i)]
(x : Ξ (i : ΞΉ), πΈ i)
(i : ΞΉ) :
theorem
pi.exp_def
(π : Type u_1)
[is_R_or_C π]
{ΞΉ : Type u_2}
{πΈ : ΞΉ β Type u_3}
[fintype ΞΉ]
[Ξ (i : ΞΉ), normed_ring (πΈ i)]
[Ξ (i : ΞΉ), normed_algebra π (πΈ i)]
[β (i : ΞΉ), complete_space (πΈ i)]
(x : Ξ (i : ΞΉ), πΈ i) :
theorem
function.update_exp
(π : Type u_1)
[is_R_or_C π]
{ΞΉ : Type u_2}
{πΈ : ΞΉ β Type u_3}
[fintype ΞΉ]
[decidable_eq ΞΉ]
[Ξ (i : ΞΉ), normed_ring (πΈ i)]
[Ξ (i : ΞΉ), normed_algebra π (πΈ i)]
[β (i : ΞΉ), complete_space (πΈ i)]
(x : Ξ (i : ΞΉ), πΈ i)
(j : ΞΉ)
(xj : πΈ j) :
function.update (exp π x) j (exp π xj) = exp π (function.update x j xj)
theorem
algebra_map_exp_comm
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_ring πΈ]
[normed_algebra π πΈ]
(x : π) :
β(algebra_map π πΈ) (exp π x) = exp π (β(algebra_map π πΈ) x)
theorem
norm_exp_series_div_summable
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
(x : πΈ) :
theorem
exp_series_div_summable
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_series_div_has_sum_exp
(π : Type u_1)
{πΈ : Type u_2}
[is_R_or_C π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_neg
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(x : πΈ) :
theorem
exp_zsmul
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_division_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
(z : β€)
(x : πΈ) :
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_sum
{π : Type u_1}
{πΈ : Type u_2}
[is_R_or_C π]
[normed_comm_ring πΈ]
[normed_algebra π πΈ]
[complete_space πΈ]
{ΞΉ : Type u_3}
(s : finset ΞΉ)
(f : ΞΉ β πΈ) :
A version of exp_sum_of_commute for a commutative Banach-algebra.
theorem
exp_series_eq_exp_series
(π : Type u_1)
(π' : Type u_2)
(πΈ : Type u_3)
[field π]
[field π']
[ring πΈ]
[algebra π πΈ]
[algebra π' πΈ]
[topological_space πΈ]
[topological_ring πΈ]
(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)
[field π]
[field π']
[ring πΈ]
[algebra π πΈ]
[algebra π' πΈ]
[topological_space πΈ]
[topological_ring πΈ] :
If a normed ring πΈ is a normed algebra over two fields, then they define the same
exponential function on πΈ.
@[simp, norm_cast]
A version of complex.of_real_exp for exp instead of complex.exp