mathlib3 documentation

analysis.special_functions.exp_deriv

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.

@[simp]
@[simp]
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) :
deriv (λ (x : 𝕜), cexp (f x)) x = cexp (f x) * deriv 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) :
cont_diff 𝕜 n (λ (x : E), cexp (f x))
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
@[simp]
@[simp]

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
@[simp]
theorem deriv_exp {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), rexp (f x)) x = rexp (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 cont_diff.exp {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (hf : cont_diff n f) :
cont_diff n (λ (x : E), rexp (f x))
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) :
fderiv (λ (x : E), rexp (f x)) x = rexp (f x) fderiv f x