mathlib documentation

analysis.special_functions.exp_deriv

Complex and real exponential #

In this file we prove that complex.exp and real.exp are infinitely smooth functions.

Tags #

exp, derivative

The complex exponential is everywhere differentiable, with the derivative exp x.

theorem has_strict_deriv_at.cexp {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_at.cexp {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_within_at.cexp {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') s x
theorem deriv_within_cexp {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.exp (f x)) s x = (complex.exp (f x)) * deriv_within f s x
@[simp]
theorem deriv_cexp {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.exp (f x)) x = (complex.exp (f x)) * deriv f x
theorem has_strict_deriv_at.cexp_real {f : } {f' : } {x : } (h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_at.cexp_real {f : } {f' : } {x : } (h : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_within_at.cexp_real {f : } {f' : } {x : } {s : set } (h : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') s x
theorem has_strict_fderiv_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem has_fderiv_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') s x
theorem has_fderiv_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem differentiable_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.exp (f x)) s x
@[simp]
theorem differentiable_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.exp (f x)) x
theorem differentiable_on.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.exp (f x)) s
@[simp]
theorem differentiable.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.exp (f x))
theorem times_cont_diff.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.exp (f x))
theorem times_cont_diff_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.exp (f x)) x
theorem times_cont_diff_on.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.exp (f x)) s
theorem times_cont_diff_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.exp (f x)) s x

Register lemmas for the derivatives of the composition of real.exp with a differentiable function, for standalone use and use with simp.

theorem has_strict_deriv_at.exp {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') x
theorem has_deriv_at.exp {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') x
theorem has_deriv_within_at.exp {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') s x
theorem deriv_within_exp {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.exp (f x)) s x = (real.exp (f x)) * deriv_within f s x
@[simp]
theorem deriv_exp {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.exp (f x)) x = (real.exp (f x)) * deriv f x

Register lemmas for the derivatives of the composition of real.exp with a differentiable function, for standalone use and use with simp.

theorem times_cont_diff.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (hf : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.exp (f x))
theorem times_cont_diff_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.exp (f x)) x
theorem times_cont_diff_on.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.exp (f x)) s
theorem times_cont_diff_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.exp (f x)) s x
theorem has_fderiv_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') s x
theorem has_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') x
theorem has_strict_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') x
theorem differentiable_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.exp (f x)) s x
@[simp]
theorem differentiable_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.exp (f x)) x
theorem differentiable_on.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.exp (f x)) s
@[simp]
theorem differentiable.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.exp (f x))
theorem fderiv_within_exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.exp (f x)) s x = real.exp (f x) fderiv_within f s x
@[simp]
theorem fderiv_exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.exp (f x)) x = real.exp (f x) fderiv f x