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

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