mathlib documentation

analysis.special_functions.exponential

Calculus results on exponential in a Banach algebra #

In this file, we prove basic properties about the derivative of the exponential map exp 𝕂 in a Banach algebra 𝔸 over a field 𝕂. We keep them separate from the main file analysis/normed_space/exponential in order to minimize dependencies.

Main results #

We prove most result for an arbitrary field 𝕂, and then specialize to 𝕂 = ℝ or 𝕂 = ℂ.

General case #

has_strict_fderiv_at_exp_zero_of_radius_pos : exp 𝕂 has strict Fréchet-derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero, as long as it converges on a neighborhood of zero (see also has_strict_deriv_at_exp_zero_of_radius_pos for the case 𝔸 = 𝕂)
has_strict_fderiv_at_exp_of_lt_radius : if 𝕂 has characteristic zero and 𝔸 is commutative, then given a point x in the disk of convergence, exp 𝕂 as strict Fréchet-derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at x (see also has_strict_deriv_at_exp_of_lt_radius for the case 𝔸 = 𝕂)

`𝕂 = ℝ` or `𝕂 = ℂ` #

has_strict_fderiv_at_exp_zero : exp 𝕂 has strict Fréchet-derivative 1 : 𝔸 →L[𝕂] 𝔸 at zero (see also has_strict_deriv_at_exp_zero for the case 𝔸 = 𝕂)
has_strict_fderiv_at_exp : if 𝔸 is commutative, then given any point x, exp 𝕂 as strict Fréchet-derivative exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸 at x (see also has_strict_deriv_at_exp for the case 𝔸 = 𝕂)

Compatibilty with `real.exp` and `complex.exp` #

complex.exp_eq_exp_ℂ : complex.exp = exp ℂ ℂ
real.exp_eq_exp_ℝ : real.exp = exp ℝ ℝ

theorem has_strict_fderiv_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_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} [nontrivially_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 has_fderiv_at_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [nontrivially_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} [nontrivially_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} [nontrivially_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} [nontrivially_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} [nontrivially_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} [nontrivially_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 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 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 complex.exp_eq_exp_ℂ :

complex.exp = exp ℂ

theorem real.exp_eq_exp_ℝ :

real.exp = exp ℝ