HepLean 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 #

source
theorem analyticOnNhd_cexp :
AnalyticOnNhd ℂ Complex.exp Set.univ

exp is entire

source
theorem analyticOn_cexp :
AnalyticOn ℂ Complex.exp Set.univ
source
theorem analyticAt_cexp {z : ℂ} :
AnalyticAt ℂ Complex.exp z

exp is analytic at any point

source
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

source
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
source
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

source
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
source
theorem Complex.hasDerivAt_exp (x : ℂ) :
HasDerivAt Complex.exp (Complex.exp x) x

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

source
theorem Complex.differentiable_exp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 ℂ] :
Differentiable 𝕜 Complex.exp
source
theorem Complex.differentiableAt_exp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 ℂ] {x : ℂ} :
DifferentiableAt 𝕜 Complex.exp x
source
@[simp]
theorem Complex.deriv_exp :
deriv Complex.exp = Complex.exp
source
@[simp]
theorem Complex.iter_deriv_exp (n : ℕ) :
deriv^[n] Complex.exp = Complex.exp
source
theorem Complex.contDiff_exp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 ℂ] {n : ℕ∞} :
ContDiff 𝕜 n Complex.exp
source
theorem Complex.hasStrictDerivAt_exp (x : ℂ) :
HasStrictDerivAt Complex.exp (Complex.exp x) x
source
theorem Complex.hasStrictFDerivAt_exp_real (x : ℂ) :
HasStrictFDerivAt Complex.exp (Complex.exp x • 1) x
source
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
source
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
source
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
source
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
source
@[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
source
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
source
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
source
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
source
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
source
@[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
source
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
source
@[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)
source
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)
source
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
source
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
source
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
source
@[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 #

source
theorem analyticOnNhd_rexp :
AnalyticOnNhd ℝ Real.exp Set.univ

exp is entire

source
theorem analyticOn_rexp :
AnalyticOn ℝ Real.exp Set.univ
source
theorem analyticAt_rexp {x : ℝ} :
AnalyticAt ℝ Real.exp x

exp is analytic at any point

source
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

source
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
source
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

source
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
source
theorem Real.hasStrictDerivAt_exp (x : ℝ) :
HasStrictDerivAt Real.exp (Real.exp x) x
source
theorem Real.hasDerivAt_exp (x : ℝ) :
HasDerivAt Real.exp (Real.exp x) x
source
theorem Real.contDiff_exp {n : ℕ∞} :
ContDiff ℝ n Real.exp
source
theorem Real.differentiable_exp :
Differentiable ℝ Real.exp
source
theorem Real.differentiableAt_exp {x : ℝ} :
DifferentiableAt ℝ Real.exp x
source
@[simp]
theorem Real.deriv_exp :
deriv Real.exp = Real.exp
source
@[simp]
theorem Real.iter_deriv_exp (n : ℕ) :
deriv^[n] Real.exp = Real.exp

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

source
theorem HasStrictDerivAt.exp {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => Real.exp (f x)) (Real.exp (f x) * f') x
source
theorem HasDerivAt.exp {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => Real.exp (f x)) (Real.exp (f x) * f') x
source
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
source
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
source
@[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.

source
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)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
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
source
@[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)
source
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
source
@[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
source
@[simp]
theorem iteratedDeriv_exp_const_mul (n : ℕ) (c : ℝ) :
(iteratedDeriv n fun (s : ℝ) => Real.exp (c * s)) = fun (s : ℝ) => c ^ n * Real.exp (c * s)