mathlib3 documentation

analysis.normed_space.exponential

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 #

𝕂 = ℝ or 𝕂 = β„‚ #

Other useful compatibility results #

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
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
theorem exp_series_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) (n : β„•) :
⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x) = (↑(n.factorial))⁻¹ β€’ x ^ n
theorem exp_series_apply_eq' {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) :
(Ξ» (n : β„•), ⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)) = Ξ» (n : β„•), (↑(n.factorial))⁻¹ β€’ x ^ n
theorem exp_series_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) :
(exp_series 𝕂 𝔸).sum x = βˆ‘' (n : β„•), (↑(n.factorial))⁻¹ β€’ x ^ n
theorem exp_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] :
exp 𝕂 = Ξ» (x : 𝔸), βˆ‘' (n : β„•), (↑(n.factorial))⁻¹ β€’ x ^ n
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_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [t2_space 𝔸] :
exp 𝕂 0 = 1
@[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) :
commute x (exp 𝕂 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) :
commute (exp 𝕂 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) :
commute (exp 𝕂 x) (exp 𝕂 y)
theorem exp_series_apply_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) (n : β„•) :
⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x) = x ^ n / ↑(n.factorial)
theorem exp_series_apply_eq_div' {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) :
(Ξ» (n : β„•), ⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)) = Ξ» (n : β„•), x ^ n / ↑(n.factorial)
theorem exp_series_sum_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) :
(exp_series 𝕂 𝔸).sum x = βˆ‘' (n : β„•), x ^ n / ↑(n.factorial)
theorem exp_eq_tsum_div {𝕂 : Type u_1} {𝔸 : Type u_2} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] :
exp 𝕂 = Ξ» (x : 𝔸), βˆ‘' (n : β„•), x ^ n / ↑(n.factorial)
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) :
summable (Ξ» (n : β„•), ‖⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)β€–)
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) :
has_sum (Ξ» (n : β„•), ⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)) (exp 𝕂 x)
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) :
has_sum (Ξ» (n : β„•), (↑(n.factorial))⁻¹ β€’ x ^ n) (exp 𝕂 x)
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) :
exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 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 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
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) :
is_unit (exp 𝕂 x)
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)] :
β…Ÿ (exp 𝕂 x) = 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) :
⇑f (exp 𝕂 x) = exp 𝕂 (⇑f x)

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) :
summable (Ξ» (n : β„•), x ^ n / ↑(n.factorial))
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) :
has_sum (Ξ» (n : β„•), x ^ n / ↑(n.factorial)) (exp 𝕂 x)
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) :
exp 𝕂 (-x) = (exp 𝕂 x)⁻¹
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) :
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.

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 : 𝔸) :
summable (Ξ» (n : β„•), ‖⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), 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 : 𝔸) :
has_sum (Ξ» (n : β„•), ⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)) (exp 𝕂 x)
theorem exp_series_has_sum_exp' {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) :
has_sum (Ξ» (n : β„•), (↑(n.factorial))⁻¹ β€’ x ^ n) (exp 𝕂 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) :
exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 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
theorem is_unit_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) :
is_unit (exp 𝕂 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)] :
β…Ÿ (exp 𝕂 x) = 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 𝔸) :
exp 𝕂 x ∈ unitary 𝔸
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 : 𝔸) :
exp 𝕂 (n β€’ x) = exp 𝕂 x ^ n
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 : 𝔸) :
⇑f (exp 𝕂 x) = exp 𝕂 (⇑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 : 𝔸) :
exp 𝕂 (g β€’ x) = g β€’ exp 𝕂 x
theorem exp_units_conj (𝕂 : Type u_1) {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (y : 𝔸ˣ) (x : 𝔸) :
exp 𝕂 (↑y * x * ↑y⁻¹) = ↑y * exp 𝕂 x * ↑y⁻¹
theorem exp_units_conj' (𝕂 : Type u_1) {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (y : 𝔸ˣ) (x : 𝔸) :
exp 𝕂 (↑y⁻¹ * x * ↑y) = ↑y⁻¹ * exp 𝕂 x * ↑y
@[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 : 𝔸 Γ— 𝔹) :
(exp 𝕂 x).fst = exp 𝕂 x.fst
@[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 : 𝔸 Γ— 𝔹) :
(exp 𝕂 x).snd = exp 𝕂 x.snd
@[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 : ΞΉ) :
exp 𝕂 x i = exp 𝕂 (x 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) :
exp 𝕂 x = Ξ» (i : ΞΉ), exp 𝕂 (x 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 : 𝔸) :
summable (Ξ» (n : β„•), x ^ n / ↑(n.factorial))
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 : 𝔸) :
has_sum (Ξ» (n : β„•), x ^ n / ↑(n.factorial)) (exp 𝕂 x)
theorem exp_neg {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) :
exp 𝕂 (-x) = (exp 𝕂 x)⁻¹
theorem exp_zsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (z : β„€) (x : 𝔸) :
exp 𝕂 (z β€’ x) = exp 𝕂 x ^ z
theorem exp_conj {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (y x : 𝔸) (hy : y β‰  0) :
exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹
theorem exp_conj' {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (y x : 𝔸) (hy : y β‰  0) :
exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * exp 𝕂 x * y
theorem exp_add {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] {x y : 𝔸} :
exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 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 : ΞΉ β†’ 𝔸) :
exp 𝕂 (s.sum (Ξ» (i : ΞΉ), f i)) = s.prod (Ξ» (i : ΞΉ), exp 𝕂 (f i))

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 𝔸] :
exp 𝕂 = exp 𝕂'

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