Complex and real exponential #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that complex.exp and real.exp are infinitely smooth functions.
Tags #
exp, derivative
The complex exponential is everywhere differentiable, with the derivative exp x.
theorem
complex.differentiable_exp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[normed_algebra 𝕜 ℂ] :
theorem
complex.differentiable_at_exp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[normed_algebra 𝕜 ℂ]
{x : ℂ} :
theorem
complex.cont_diff_exp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[normed_algebra 𝕜 ℂ]
{n : ℕ∞} :
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
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
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
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
@[simp]
theorem
deriv_cexp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[normed_algebra 𝕜 ℂ]
{f : 𝕜 → ℂ}
{x : 𝕜}
(hc : differentiable_at 𝕜 f x) :
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
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
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
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
@[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
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
@[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))
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) :
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
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
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
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 : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), rexp (f x)) (rexp (f x) * f') x
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
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
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
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}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : ℕ∞}
(hf : cont_diff ℝ n f) :
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
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
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
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
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
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
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
@[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
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
@[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))
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
@[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) :