mathlib documentation

analysis.normed_space.exponential

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 basic results, as described below.

Main result #

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) [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
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
theorem exp_series_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] (x : 𝔸) (n : β„•) :
⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x) = (1 / ↑n!) β€’ x ^ n
theorem exp_series_apply_eq' {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] (x : 𝔸) :
(Ξ» (n : β„•), ⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)) = Ξ» (n : β„•), (1 / ↑n!) β€’ x ^ n
theorem exp_series_apply_eq_field {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] (x : 𝕂) (n : β„•) :
⇑(exp_series 𝕂 𝕂 n) (Ξ» (_x : fin n), x) = x ^ n / ↑n!
theorem exp_series_apply_eq_field' {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] (x : 𝕂) :
(Ξ» (n : β„•), ⇑(exp_series 𝕂 𝕂 n) (Ξ» (_x : fin n), x)) = Ξ» (n : β„•), x ^ n / ↑n!
theorem exp_series_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] (x : 𝔸) :
(exp_series 𝕂 𝔸).sum x = βˆ‘' (n : β„•), (1 / ↑n!) β€’ x ^ n
theorem exp_series_sum_eq_field {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] (x : 𝕂) :
(exp_series 𝕂 𝕂).sum x = βˆ‘' (n : β„•), x ^ n / ↑n!
theorem exp_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] :
exp 𝕂 𝔸 = Ξ» (x : 𝔸), βˆ‘' (n : β„•), (1 / ↑n!) β€’ x ^ n
theorem exp_eq_tsum_field {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] :
exp 𝕂 𝕂 = Ξ» (x : 𝕂), βˆ‘' (n : β„•), x ^ n / ↑n!
theorem exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] :
exp 𝕂 𝔸 0 = 1
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) :
summable (Ξ» (n : β„•), βˆ₯⇑(exp_series 𝕂 𝔸 n) (Ξ» (_x : fin n), x)βˆ₯)
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) :
summable (Ξ» (n : β„•), (1 / ↑n!) β€’ x ^ n)
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) :
summable (Ξ» (n : β„•), x ^ n / ↑n!)
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) :
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} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (hx : x ∈ emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_sum (Ξ» (n : β„•), (1 / ↑n!) β€’ x ^ n) (exp 𝕂 𝔸 x)
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) :
has_sum (Ξ» (n : β„•), x ^ n / ↑n!) (exp 𝕂 𝕂 x)
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 has_strict_fderiv_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_strict_fderiv_at (exp 𝕂 𝔸) 1 0

The exponential in a Banach-algebra 𝔸 over a normed field 𝕂 has strict FrΓ©chet-derivative 1 : 𝔸 β†’L[𝕂] 𝔸 at zero, as long as it converges on a neighborhood of zero.

theorem has_fderiv_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_fderiv_at (exp 𝕂 𝔸) 1 0

The exponential in a Banach-algebra 𝔸 over a normed field 𝕂 has FrΓ©chet-derivative 1 : 𝔸 β†’L[𝕂] 𝔸 at zero, as long as it converges on a neighborhood of zero.

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) :
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).

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) :
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 has_fderiv_at_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] [char_zero 𝕂] {x : 𝔸} (hx : x ∈ emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x β€’ 1) x

The exponential map in a commutative Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero has FrΓ©chet-derivative exp 𝕂 𝔸 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x in the disk of convergence.

theorem has_strict_fderiv_at_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [nondiscrete_normed_field 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] [char_zero 𝕂] {x : 𝔸} (hx : x ∈ emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x β€’ 1) x

The exponential map in a commutative Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero has strict FrΓ©chet-derivative exp 𝕂 𝔸 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x in the disk of convergence.

theorem has_strict_deriv_at_exp_of_mem_ball {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] [complete_space 𝕂] [char_zero 𝕂] {x : 𝕂} (hx : x ∈ emetric.ball 0 (exp_series 𝕂 𝕂).radius) :
has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x

The exponential map in a complete normed field 𝕂 of characteristic zero has strict derivative exp 𝕂 𝕂 x at any point x in the disk of convergence.

theorem has_deriv_at_exp_of_mem_ball {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] [complete_space 𝕂] [char_zero 𝕂] {x : 𝕂} (hx : x ∈ emetric.ball 0 (exp_series 𝕂 𝕂).radius) :
has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x

The exponential map in a complete normed field 𝕂 of characteristic zero has derivative exp 𝕂 𝕂 x at any point x in the disk of convergence.

theorem has_strict_deriv_at_exp_zero_of_radius_pos {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] [complete_space 𝕂] (h : 0 < (exp_series 𝕂 𝕂).radius) :
has_strict_deriv_at (exp 𝕂 𝕂) 1 0

The exponential map in a complete normed field 𝕂 of characteristic zero has strict derivative 1 at zero, as long as it converges on a neighborhood of zero.

theorem has_deriv_at_exp_zero_of_radius_pos {𝕂 : Type u_1} [nondiscrete_normed_field 𝕂] [complete_space 𝕂] (h : 0 < (exp_series 𝕂 𝕂).radius) :
has_deriv_at (exp 𝕂 𝕂) 1 0

The exponential map in a complete normed field 𝕂 of characteristic zero has derivative 1 at zero, as long as it converges on a neighborhood of zero.

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 norm_exp_series_field_summable {𝕂 : Type u_1} [is_R_or_C 𝕂] (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 : 𝔸) :
summable (Ξ» (n : β„•), (1 / ↑n!) β€’ x ^ n)
theorem exp_series_field_summable {𝕂 : Type u_1} [is_R_or_C 𝕂] (x : 𝕂) :
summable (Ξ» (n : β„•), x ^ n / ↑n!)
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 : β„•), (1 / ↑n!) β€’ x ^ n) (exp 𝕂 𝔸 x)
theorem exp_series_field_has_sum_exp {𝕂 : Type u_1} [is_R_or_C 𝕂] (x : 𝕂) :
has_sum (Ξ» (n : β„•), x ^ n / ↑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
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 has_strict_fderiv_at_exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] :
has_strict_fderiv_at (exp 𝕂 𝔸) 1 0

The exponential in a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = β„‚ has strict FrΓ©chet-derivative 1 : 𝔸 β†’L[𝕂] 𝔸 at zero.

theorem has_fderiv_at_exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] :
has_fderiv_at (exp 𝕂 𝔸) 1 0

The exponential in a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = β„‚ has FrΓ©chet-derivative 1 : 𝔸 β†’L[𝕂] 𝔸 at zero.

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

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 comutative Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = β„‚, exp 𝕂 𝔸 (x+y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y).

theorem has_strict_fderiv_at_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] {x : 𝔸} :
has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x β€’ 1) x

The exponential map in a commutative Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = β„‚ has strict FrΓ©chet-derivative exp 𝕂 𝔸 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x.

theorem has_fderiv_at_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] {x : 𝔸} :
has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x β€’ 1) x

The exponential map in a commutative Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = β„‚ has FrΓ©chet-derivative exp 𝕂 𝔸 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸 at any point x.

theorem has_strict_deriv_at_exp {𝕂 : Type u_1} [is_R_or_C 𝕂] {x : 𝕂} :
has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x

The exponential map in 𝕂 = ℝ or 𝕂 = β„‚ has strict derivative exp 𝕂 𝕂 x at any point x.

theorem has_deriv_at_exp {𝕂 : Type u_1} [is_R_or_C 𝕂] {x : 𝕂} :
has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x

The exponential map in 𝕂 = ℝ or 𝕂 = β„‚ has derivative exp 𝕂 𝕂 x at any point x.

theorem has_strict_deriv_at_exp_zero {𝕂 : Type u_1} [is_R_or_C 𝕂] :
has_strict_deriv_at (exp 𝕂 𝕂) 1 0

The exponential map in 𝕂 = ℝ or 𝕂 = β„‚ has strict derivative 1 at zero.

theorem has_deriv_at_exp_zero {𝕂 : Type u_1} [is_R_or_C 𝕂] :
has_deriv_at (exp 𝕂 𝕂) 1 0

The exponential map in 𝕂 = ℝ or 𝕂 = β„‚ has derivative 1 at zero.

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

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same exponential function on 𝔸.