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

source
theorem complex.has_deriv_at_exp (x : β„‚) :
has_deriv_at cexp (cexp x) x

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

source
theorem complex.differentiable_exp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] :
differentiable π•œ cexp
source
theorem complex.differentiable_at_exp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {x : β„‚} :
differentiable_at π•œ cexp x
source
@[simp]
theorem complex.deriv_exp  :
deriv cexp = cexp
source
@[simp]
theorem complex.iter_deriv_exp (n : β„•) :
deriv^[n] cexp = cexp
source
theorem complex.cont_diff_exp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {n : β„•βˆž} :
cont_diff π•œ n cexp
source
theorem complex.has_strict_deriv_at_exp (x : β„‚) :
has_strict_deriv_at cexp (cexp x) x
source
theorem complex.has_strict_fderiv_at_exp_real (x : β„‚) :
has_strict_fderiv_at cexp (cexp x β€’ 1) x
source
theorem complex.is_open_map_exp  :
is_open_map cexp
source
theorem has_strict_deriv_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {f : π•œ β†’ β„‚} {f' : β„‚} {x : π•œ} (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (Ξ» (x : π•œ), cexp (f x)) (cexp (f x) * f') x
source
theorem has_deriv_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {f : π•œ β†’ β„‚} {f' : β„‚} {x : π•œ} (hf : has_deriv_at f f' x) :
has_deriv_at (Ξ» (x : π•œ), cexp (f x)) (cexp (f x) * f') x
source
theorem has_deriv_within_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {f : π•œ β†’ β„‚} {f' : β„‚} {x : π•œ} {s : set π•œ} (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (Ξ» (x : π•œ), cexp (f x)) (cexp (f x) * f') s x
source
theorem deriv_within_cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {f : π•œ β†’ β„‚} {x : π•œ} {s : set π•œ} (hf : differentiable_within_at π•œ f s x) (hxs : unique_diff_within_at π•œ s x) :
deriv_within (Ξ» (x : π•œ), cexp (f x)) s x = cexp (f x) * deriv_within f s x
source
@[simp]
theorem deriv_cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {f : π•œ β†’ β„‚} {x : π•œ} (hc : differentiable_at π•œ f x) :
deriv (Ξ» (x : π•œ), cexp (f x)) x = cexp (f x) * deriv f x
source
theorem has_strict_fderiv_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_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), cexp (f x)) (cexp (f x) β€’ f') x
source
theorem has_fderiv_within_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_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), cexp (f x)) (cexp (f x) β€’ f') s x
source
theorem has_fderiv_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {f' : E β†’L[π•œ] β„‚} {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (Ξ» (x : E), cexp (f x)) (cexp (f x) β€’ f') x
source
theorem differentiable_within_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {x : E} {s : set E} (hf : differentiable_within_at π•œ f s x) :
differentiable_within_at π•œ (Ξ» (x : E), cexp (f x)) s x
source
@[simp]
theorem differentiable_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {x : E} (hc : differentiable_at π•œ f x) :
differentiable_at π•œ (Ξ» (x : E), cexp (f x)) x
source
theorem differentiable_on.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {s : set E} (hc : differentiable_on π•œ f s) :
differentiable_on π•œ (Ξ» (x : E), cexp (f x)) s
source
@[simp]
theorem differentiable.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} (hc : differentiable π•œ f) :
differentiable π•œ (Ξ» (x : E), cexp (f x))
source
theorem cont_diff.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {n : β„•βˆž} (h : cont_diff π•œ n f) :
cont_diff π•œ n (Ξ» (x : E), cexp (f x))
source
theorem cont_diff_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {x : E} {n : β„•βˆž} (hf : cont_diff_at π•œ n f x) :
cont_diff_at π•œ n (Ξ» (x : E), cexp (f x)) x
source
theorem cont_diff_on.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {s : set E} {n : β„•βˆž} (hf : cont_diff_on π•œ n f s) :
cont_diff_on π•œ n (Ξ» (x : E), cexp (f x)) s
source
theorem cont_diff_within_at.cexp {π•œ : Type u_1} [nontrivially_normed_field π•œ] [normed_algebra π•œ β„‚] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {f : E β†’ β„‚} {x : E} {s : set E} {n : β„•βˆž} (hf : cont_diff_within_at π•œ n f s x) :
cont_diff_within_at π•œ n (Ξ» (x : E), cexp (f x)) s x
source
theorem real.has_strict_deriv_at_exp (x : ℝ) :
has_strict_deriv_at rexp (rexp x) x
source
theorem real.has_deriv_at_exp (x : ℝ) :
has_deriv_at rexp (rexp x) x
source
theorem real.cont_diff_exp {n : β„•βˆž} :
cont_diff ℝ n rexp
source
theorem real.differentiable_exp  :
differentiable ℝ rexp
source
theorem real.differentiable_at_exp {x : ℝ} :
differentiable_at ℝ rexp x
source
@[simp]
theorem real.deriv_exp  :
deriv rexp = rexp
source
@[simp]
theorem real.iter_deriv_exp (n : β„•) :
deriv^[n] rexp = rexp

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

source
theorem has_strict_deriv_at.exp {f : ℝ β†’ ℝ} {f' x : ℝ} (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (Ξ» (x : ℝ), rexp (f x)) (rexp (f x) * f') x
source
theorem has_deriv_at.exp {f : ℝ β†’ ℝ} {f' x : ℝ} (hf : has_deriv_at f f' x) :
has_deriv_at (Ξ» (x : ℝ), rexp (f x)) (rexp (f x) * f') x
source
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 : ℝ), rexp (f x)) (rexp (f x) * f') s x
source
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 : ℝ), rexp (f x)) s x = rexp (f x) * deriv_within f s x
source
@[simp]
theorem deriv_exp {f : ℝ β†’ ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :
deriv (Ξ» (x : ℝ), rexp (f x)) x = rexp (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.

source
theorem cont_diff.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {n : β„•βˆž} (hf : cont_diff ℝ n f) :
cont_diff ℝ n (Ξ» (x : E), rexp (f x))
source
theorem cont_diff_at.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {x : E} {n : β„•βˆž} (hf : cont_diff_at ℝ n f x) :
cont_diff_at ℝ n (Ξ» (x : E), rexp (f x)) x
source
theorem cont_diff_on.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {s : set E} {n : β„•βˆž} (hf : cont_diff_on ℝ n f s) :
cont_diff_on ℝ n (Ξ» (x : E), rexp (f x)) s
source
theorem cont_diff_within_at.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {x : E} {s : set E} {n : β„•βˆž} (hf : cont_diff_within_at ℝ n f s x) :
cont_diff_within_at ℝ n (Ξ» (x : E), rexp (f x)) s x
source
theorem has_fderiv_within_at.exp {E : Type u_1} [normed_add_comm_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), rexp (f x)) (rexp (f x) β€’ f') s x
source
theorem has_fderiv_at.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {f' : E β†’L[ℝ] ℝ} {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (Ξ» (x : E), rexp (f x)) (rexp (f x) β€’ f') x
source
theorem has_strict_fderiv_at.exp {E : Type u_1} [normed_add_comm_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), rexp (f x)) (rexp (f x) β€’ f') x
source
theorem differentiable_within_at.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {x : E} {s : set E} (hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (Ξ» (x : E), rexp (f x)) s x
source
@[simp]
theorem differentiable_at.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {x : E} (hc : differentiable_at ℝ f x) :
differentiable_at ℝ (Ξ» (x : E), rexp (f x)) x
source
theorem differentiable_on.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {s : set E} (hc : differentiable_on ℝ f s) :
differentiable_on ℝ (Ξ» (x : E), rexp (f x)) s
source
@[simp]
theorem differentiable.exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} (hc : differentiable ℝ f) :
differentiable ℝ (Ξ» (x : E), rexp (f x))
source
theorem fderiv_within_exp {E : Type u_1} [normed_add_comm_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), rexp (f x)) s x = rexp (f x) β€’ fderiv_within ℝ f s x
source
@[simp]
theorem fderiv_exp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E β†’ ℝ} {x : E} (hc : differentiable_at ℝ f x) :
fderiv ℝ (Ξ» (x : E), rexp (f x)) x = rexp (f x) β€’ fderiv ℝ f x