mathlib3 documentation

analysis.special_functions.exponential

Calculus results on 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 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 #

𝕂 = ℝ or 𝕂 = ℂ #

Compatibilty with real.exp and complex.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) :

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.

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 𝔸] :

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 𝕂] :

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.

Derivative of $\exp (ux)$ by $u$ #

Note that since for x : 𝔸 we have normed_ring 𝔸 not normed_comm_ring 𝔸, we cannot deduce these results from has_fderiv_at_exp_of_mem_ball applied to the algebra 𝔸.

One possible solution for that would be to apply has_fderiv_at_exp_of_mem_ball to the commutative algebra algebra.elemental_algebra 𝕊 x. Unfortunately we don't have all the required API, so we leave that to a future refactor (see leanprover-community/mathlib#19062 for discussion).

We could also go the other way around and deduce has_fderiv_at_exp_of_mem_ball from has_fderiv_at_exp_smul_const_of_mem_ball applied to 𝕊 := 𝔸, x := (1 : 𝔸), and t := x. However, doing so would make the aformentioned elemental_algebra refactor harder, so for now we just prove these two lemmas independently.

A last strategy would be to deduce everything from the more general non-commutative case, $$\frac{d}{dt}e^{x(t)} = \int_0^1 e^{sx(t)} \left(\frac{d}{dt}e^{x(t)}\right) e^{(1-s)x(t)} ds$$ but this is harder to prove, and typically is shown by going via these results first.

TODO: prove this result too!

theorem has_fderiv_at_exp_smul_const_of_mem_ball (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_space 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) (exp 𝕂 (t x) 1.smul_right x) t
theorem has_fderiv_at_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_space 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) ((1.smul_right x).smul_right (exp 𝕂 (t x))) t
theorem has_strict_fderiv_at_exp_smul_const_of_mem_ball (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_space 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_strict_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) (exp 𝕂 (t x) 1.smul_right x) t
theorem has_strict_fderiv_at_exp_smul_const_of_mem_ball' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_space 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_strict_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) ((1.smul_right x).smul_right (exp 𝕂 (t x))) t
theorem has_strict_deriv_at_exp_smul_const_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_strict_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem has_strict_deriv_at_exp_smul_const_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_strict_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem has_deriv_at_exp_smul_const_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem has_deriv_at_exp_smul_const_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_3} [nontrivially_normed_field 𝕂] [char_zero 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) (htx : t x emetric.ball 0 (exp_series 𝕂 𝔸).radius) :
has_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem has_fderiv_at_exp_smul_const (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_algebra 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) :
has_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) (exp 𝕂 (t x) 1.smul_right x) t
theorem has_fderiv_at_exp_smul_const' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_algebra 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) :
has_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) ((1.smul_right x).smul_right (exp 𝕂 (t x))) t
theorem has_strict_fderiv_at_exp_smul_const (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_algebra 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) :
has_strict_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) (exp 𝕂 (t x) 1.smul_right x) t
theorem has_strict_fderiv_at_exp_smul_const' (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_comm_ring 𝕊] [normed_ring 𝔸] [normed_algebra 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸] [is_scalar_tower 𝕂 𝕊 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕊) :
has_strict_fderiv_at (λ (u : 𝕊), exp 𝕂 (u x)) ((1.smul_right x).smul_right (exp 𝕂 (t x))) t
theorem has_strict_deriv_at_exp_smul_const {𝕂 : Type u_1} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) :
has_strict_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem has_strict_deriv_at_exp_smul_const' {𝕂 : Type u_1} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) :
has_strict_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t
theorem has_deriv_at_exp_smul_const {𝕂 : Type u_1} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) :
has_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (exp 𝕂 (t x) * x) t
theorem has_deriv_at_exp_smul_const' {𝕂 : Type u_1} {𝔸 : Type u_3} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (x : 𝔸) (t : 𝕂) :
has_deriv_at (λ (u : 𝕂), exp 𝕂 (u x)) (x * exp 𝕂 (t x)) t