Documentation

Mathlib.Analysis.SpecialFunctions.ExpDeriv

Complex and real exponential #

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

Tags #

exp, derivative

Complex.exp #

exp is analytic at any point

theorem AnalyticAt.cexp {E : Type} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (fa : AnalyticAt f x) :
AnalyticAt (fun (z : E) => Complex.exp (f z)) x

exp ∘ f is analytic

theorem AnalyticWithinAt.cexp {E : Type} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (fa : AnalyticWithinAt f s x) :
AnalyticWithinAt (fun (z : E) => Complex.exp (f z)) s x
theorem AnalyticOnNhd.cexp {E : Type} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (fs : AnalyticOnNhd f s) :
AnalyticOnNhd (fun (z : E) => Complex.exp (f z)) s

exp ∘ f is analytic

theorem AnalyticOn.cexp {E : Type} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (fs : AnalyticOn f s) :
AnalyticOn (fun (z : E) => Complex.exp (f z)) s

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

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

Real.exp #

exp is analytic at any point

theorem AnalyticAt.rexp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (fa : AnalyticAt f x) :
AnalyticAt (fun (z : E) => Real.exp (f z)) x

exp ∘ f is analytic

theorem AnalyticWithinAt.rexp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {x : E} (fa : AnalyticWithinAt f s x) :
AnalyticWithinAt (fun (z : E) => Real.exp (f z)) s x
theorem AnalyticOnNhd.rexp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (fs : AnalyticOnNhd f s) :
AnalyticOnNhd (fun (z : E) => Real.exp (f z)) s

exp ∘ f is analytic

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