# Complex and real exponential #

In this file we prove that Complex.exp and Real.exp are infinitely smooth functions.

exp, derivative

## Complex.exp#

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

theorem Complex.differentiable_exp {𝕜 : Type u_1} [] :
theorem Complex.differentiableAt_exp {𝕜 : Type u_1} [] {x : } :
@[simp]
theorem Complex.contDiff_exp {𝕜 : Type u_1} [] {n : ℕ∞} :
theorem HasStrictDerivAt.cexp {𝕜 : Type u_1} [] {f : 𝕜} {f' : } {x : 𝕜} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : 𝕜) => (f x).exp) ((f x).exp * f') x
theorem HasDerivAt.cexp {𝕜 : Type u_1} [] {f : 𝕜} {f' : } {x : 𝕜} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : 𝕜) => (f x).exp) ((f x).exp * f') x
theorem HasDerivWithinAt.cexp {𝕜 : Type u_1} [] {f : 𝕜} {f' : } {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : 𝕜) => (f x).exp) ((f x).exp * f') s x
theorem derivWithin_cexp {𝕜 : Type u_1} [] {f : 𝕜} {x : 𝕜} {s : Set 𝕜} (hf : ) (hxs : ) :
derivWithin (fun (x : 𝕜) => (f x).exp) s x = (f x).exp * derivWithin f s x
@[simp]
theorem deriv_cexp {𝕜 : Type u_1} [] {f : 𝕜} {x : 𝕜} (hc : ) :
deriv (fun (x : 𝕜) => (f x).exp) x = (f x).exp * deriv f x
theorem HasStrictFDerivAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {f' : E →L[𝕜] } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => (f x).exp) ((f x).exp f') x
theorem HasFDerivWithinAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {f' : E →L[𝕜] } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => (f x).exp) ((f x).exp f') s x
theorem HasFDerivAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {f' : E →L[𝕜] } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => (f x).exp) ((f x).exp f') x
theorem DifferentiableWithinAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt 𝕜 (fun (x : E) => (f x).exp) s x
@[simp]
theorem DifferentiableAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {x : E} (hc : ) :
DifferentiableAt 𝕜 (fun (x : E) => (f x).exp) x
theorem DifferentiableOn.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn 𝕜 (fun (x : E) => (f x).exp) s
@[simp]
theorem Differentiable.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} (hc : ) :
Differentiable 𝕜 fun (x : E) => (f x).exp
theorem ContDiff.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {n : ℕ∞} (h : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (x : E) => (f x).exp
theorem ContDiffAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt 𝕜 n f x) :
ContDiffAt 𝕜 n (fun (x : E) => (f x).exp) x
theorem ContDiffOn.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn 𝕜 n f s) :
ContDiffOn 𝕜 n (fun (x : E) => (f x).exp) s
theorem ContDiffWithinAt.cexp {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) :
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x).exp) s x
@[simp]
theorem iteratedDeriv_cexp_const_mul (n : ) (c : ) :
(iteratedDeriv n fun (s : ) => (c * s).exp) = fun (s : ) => c ^ n * (c * s).exp

## Real.exp#

@[simp]
theorem Real.deriv_exp :
@[simp]

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

theorem HasStrictDerivAt.exp {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => (f x).exp) ((f x).exp * f') x
theorem HasDerivAt.exp {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => (f x).exp) ((f x).exp * f') x
theorem HasDerivWithinAt.exp {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => (f x).exp) ((f x).exp * f') s x
theorem derivWithin_exp {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => (f x).exp) s x = (f x).exp * derivWithin f s x
@[simp]
theorem deriv_exp {f : } {x : } (hc : ) :
deriv (fun (x : ) => (f x).exp) x = (f x).exp * 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 ContDiff.exp {E : Type u_1} [] {f : E} {n : ℕ∞} (hf : ) :
ContDiff n fun (x : E) => (f x).exp
theorem ContDiffAt.exp {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => (f x).exp) x
theorem ContDiffOn.exp {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => (f x).exp) s
theorem ContDiffWithinAt.exp {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => (f x).exp) s x
theorem HasFDerivWithinAt.exp {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => (f x).exp) ((f x).exp f') s x
theorem HasFDerivAt.exp {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => (f x).exp) ((f x).exp f') x
theorem HasStrictFDerivAt.exp {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => (f x).exp) ((f x).exp f') x
theorem DifferentiableWithinAt.exp {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => (f x).exp) s x
@[simp]
theorem DifferentiableAt.exp {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => (f x).exp) x
theorem DifferentiableOn.exp {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => (f x).exp) s
@[simp]
theorem Differentiable.exp {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => (f x).exp
theorem fderivWithin_exp {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => (f x).exp) s x = (f x).exp
@[simp]
theorem fderiv_exp {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => (f x).exp) x = (f x).exp fderiv f x
@[simp]
theorem iteratedDeriv_exp_const_mul (n : ) (c : ) :
(iteratedDeriv n fun (s : ) => (c * s).exp) = fun (s : ) => c ^ n * (c * s).exp