Complex and real exponential #
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.has_strict_fderiv_at_exp_real
(x : ℂ) :
has_strict_fderiv_at complex.exp (complex.exp x • 1) x
theorem
has_strict_deriv_at.cexp
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℂ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem
has_deriv_at.cexp
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℂ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem
has_deriv_within_at.cexp
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℂ), complex.exp (f x)) ((complex.exp (f x)) * f') s x
theorem
deriv_within_cexp
{f : ℂ → ℂ}
{x : ℂ}
{s : set ℂ}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
deriv_within (λ (x : ℂ), complex.exp (f x)) s x = (complex.exp (f x)) * deriv_within f s x
@[simp]
theorem
deriv_cexp
{f : ℂ → ℂ}
{x : ℂ}
(hc : differentiable_at ℂ f x) :
deriv (λ (x : ℂ), complex.exp (f x)) x = (complex.exp (f x)) * deriv f x
theorem
has_strict_deriv_at.cexp_real
{f : ℝ → ℂ}
{f' : ℂ}
{x : ℝ}
(h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem
has_deriv_at.cexp_real
{f : ℝ → ℂ}
{f' : ℂ}
{x : ℝ}
(h : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem
has_deriv_within_at.cexp_real
{f : ℝ → ℂ}
{f' : ℂ}
{x : ℝ}
{s : set ℝ}
(h : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), complex.exp (f x)) ((complex.exp (f x)) * f') s x
theorem
has_strict_fderiv_at.cexp
{E : Type u_1}
[normed_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), complex.exp (f x)) (complex.exp (f x) • f') x
theorem
has_fderiv_within_at.cexp
{E : Type u_1}
[normed_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), complex.exp (f x)) (complex.exp (f x) • f') s x
theorem
has_fderiv_at.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) • f') x
theorem
differentiable_within_at.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x) :
differentiable_within_at ℂ (λ (x : E), complex.exp (f x)) s x
@[simp]
theorem
differentiable_at.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
differentiable_at ℂ (λ (x : E), complex.exp (f x)) x
theorem
differentiable_on.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(hc : differentiable_on ℂ f s) :
differentiable_on ℂ (λ (x : E), complex.exp (f x)) s
@[simp]
theorem
differentiable.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(hc : differentiable ℂ f) :
differentiable ℂ (λ (x : E), complex.exp (f x))
theorem
times_cont_diff.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{n : with_top ℕ}
(h : times_cont_diff ℂ n f) :
times_cont_diff ℂ n (λ (x : E), complex.exp (f x))
theorem
times_cont_diff_at.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℂ n f x) :
times_cont_diff_at ℂ n (λ (x : E), complex.exp (f x)) x
theorem
times_cont_diff_on.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℂ n f s) :
times_cont_diff_on ℂ n (λ (x : E), complex.exp (f x)) s
theorem
times_cont_diff_within_at.cexp
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℂ n f s x) :
times_cont_diff_within_at ℂ n (λ (x : E), complex.exp (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 : ℝ), real.exp (f x)) ((real.exp (f x)) * f') x
theorem
has_deriv_at.exp
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.exp (f x)) s x = (real.exp (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
times_cont_diff.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(hf : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.exp (f x))
theorem
times_cont_diff_at.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.exp (f x)) x
theorem
times_cont_diff_on.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.exp (f x)) s
theorem
times_cont_diff_within_at.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.exp (f x)) s x
theorem
has_fderiv_within_at.exp
{E : Type u_1}
[normed_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), real.exp (f x)) (real.exp (f x) • f') s x
theorem
has_fderiv_at.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f 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}
[normed_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), real.exp (f x)) (real.exp (f x) • f') x
theorem
differentiable_within_at.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.exp (f x)) s x
@[simp]
theorem
differentiable_at.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.exp (f x)) x
theorem
differentiable_on.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.exp (f x)) s
@[simp]
theorem
differentiable.exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.exp (f x))
theorem
fderiv_within_exp
{E : Type u_1}
[normed_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), real.exp (f x)) s x = real.exp (f x) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_exp
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :