# mathlibdocumentation

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

theorem complex.has_deriv_at_exp (x : ) :

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

theorem complex.differentiable_exp {𝕜 : Type u_1} [ ] :
theorem complex.differentiable_at_exp {𝕜 : Type u_1} [ ] {x : } :
@[simp]
@[simp]
theorem complex.iter_deriv_exp (n : ) :
theorem complex.cont_diff_exp {𝕜 : Type u_1} [ ] {n : ℕ∞} :
theorem has_strict_deriv_at.cexp {𝕜 : Type u_1} [ ] {f : 𝕜 → } {f' : } {x : 𝕜} (hf : x) :
has_strict_deriv_at (λ (x : 𝕜), complex.exp (f x)) (complex.exp (f x) * f') x
theorem has_deriv_at.cexp {𝕜 : Type u_1} [ ] {f : 𝕜 → } {f' : } {x : 𝕜} (hf : f' x) :
has_deriv_at (λ (x : 𝕜), complex.exp (f x)) (complex.exp (f x) * f') x
theorem has_deriv_within_at.cexp {𝕜 : Type u_1} [ ] {f : 𝕜 → } {f' : } {x : 𝕜} {s : set 𝕜} (hf : s x) :
has_deriv_within_at (λ (x : 𝕜), complex.exp (f x)) (complex.exp (f x) * f') s x
theorem deriv_within_cexp {𝕜 : Type u_1} [ ] {f : 𝕜 → } {x : 𝕜} {s : set 𝕜} (hf : x) (hxs : x) :
deriv_within (λ (x : 𝕜), complex.exp (f x)) s x = complex.exp (f x) * s x
@[simp]
theorem deriv_cexp {𝕜 : Type u_1} [ ] {f : 𝕜 → } {x : 𝕜} (hc : x) :
deriv (λ (x : 𝕜), complex.exp (f x)) x = complex.exp (f x) * x
theorem has_strict_fderiv_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {f' : E →L[𝕜] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem has_fderiv_within_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {f' : E →L[𝕜] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') s x
theorem has_fderiv_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {f' : E →L[𝕜] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem differentiable_within_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), complex.exp (f x)) s x
@[simp]
theorem differentiable_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.exp (f x)) x
theorem differentiable_on.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), complex.exp (f x)) s
@[simp]
theorem differentiable.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } (hc : f) :
(λ (x : E), complex.exp (f x))
theorem cont_diff.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {n : ℕ∞} (h : n f) :
n (λ (x : E), complex.exp (f x))
theorem cont_diff_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {x : E} {n : ℕ∞} (hf : n f x) :
n (λ (x : E), complex.exp (f x)) x
theorem cont_diff_on.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {s : set E} {n : ℕ∞} (hf : n f s) :
n (λ (x : E), complex.exp (f x)) s
theorem cont_diff_within_at.cexp {𝕜 : Type u_1} [ ] {E : Type u_2} [ E] {f : E → } {x : E} {s : set E} {n : ℕ∞} (hf : f s x) :
(λ (x : E), complex.exp (f x)) s x
theorem real.has_deriv_at_exp (x : ) :
x
theorem real.cont_diff_exp {n : ℕ∞} :
@[simp]
theorem real.deriv_exp  :
@[simp]
theorem real.iter_deriv_exp (n : ) :

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 : 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 : 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 : 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 : x) (hxs : x) :
deriv_within (λ (x : ), real.exp (f x)) s x = real.exp (f x) * s x
@[simp]
theorem deriv_exp {f : } {x : } (hc : x) :
deriv (λ (x : ), real.exp (f x)) x = real.exp (f x) * x

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

theorem cont_diff.exp {E : Type u_1} [ E] {f : E → } {n : ℕ∞} (hf : f) :
(λ (x : E), real.exp (f x))
theorem cont_diff_at.exp {E : Type u_1} [ E] {f : E → } {x : E} {n : ℕ∞} (hf : f x) :
(λ (x : E), real.exp (f x)) x
theorem cont_diff_on.exp {E : Type u_1} [ E] {f : E → } {s : set E} {n : ℕ∞} (hf : f s) :
(λ (x : E), real.exp (f x)) s
theorem cont_diff_within_at.exp {E : Type u_1} [ E] {f : E → } {x : E} {s : set E} {n : ℕ∞} (hf : s x) :
(λ (x : E), real.exp (f x)) s x
theorem has_fderiv_within_at.exp {E : Type u_1} [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : 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} [ E] {f : E → } {f' : E →L[] } {x : E} (hf : 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} [ E] {f : E → } {f' : E →L[] } {x : E} (hf : 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} [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.exp (f x)) s x
@[simp]
theorem differentiable_at.exp {E : Type u_1} [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.exp (f x)) x
theorem differentiable_on.exp {E : Type u_1} [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), real.exp (f x)) s
@[simp]
theorem differentiable.exp {E : Type u_1} [ E] {f : E → } (hc : f) :
(λ (x : E), real.exp (f x))
theorem fderiv_within_exp {E : Type u_1} [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.exp (f x)) s x = real.exp (f x) s x
@[simp]
theorem fderiv_exp {E : Type u_1} [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.exp (f x)) x = real.exp (f x) f x