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.differentiable_exp
{π : Type u_1}
[nontrivially_normed_field π]
[normed_algebra π β] :
differentiable π cexp
theorem
complex.differentiable_at_exp
{π : Type u_1}
[nontrivially_normed_field π]
[normed_algebra π β]
{x : β} :
differentiable_at π cexp x
theorem
complex.cont_diff_exp
{π : Type u_1}
[nontrivially_normed_field π]
[normed_algebra π β]
{n : ββ} :
theorem
complex.has_strict_fderiv_at_exp_real
(x : β) :
has_strict_fderiv_at cexp (cexp x β’ 1) x
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) :