Frechet derivatives of analytic functions. #
A function expressible as a power series at a point has a Frechet derivative there.
Also the special case in terms of deriv when the domain is 1-dimensional.
theorem
has_fpower_series_at.has_strict_fderiv_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{f : E β F}
{x : E}
(h : has_fpower_series_at f p x) :
has_strict_fderiv_at f (β(continuous_multilinear_curry_fin1 π E F) (p 1)) x
theorem
has_fpower_series_at.has_fderiv_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{f : E β F}
{x : E}
(h : has_fpower_series_at f p x) :
has_fderiv_at f (β(continuous_multilinear_curry_fin1 π E F) (p 1)) x
theorem
has_fpower_series_at.differentiable_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{f : E β F}
{x : E}
(h : has_fpower_series_at f p x) :
differentiable_at π f x
theorem
analytic_at.differentiable_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{x : E} :
analytic_at π f x β differentiable_at π f x
theorem
analytic_at.differentiable_within_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(h : analytic_at π f x) :
differentiable_within_at π f s x
theorem
has_fpower_series_at.fderiv_eq
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{f : E β F}
{x : E}
(h : has_fpower_series_at f p x) :
fderiv π f x = β(continuous_multilinear_curry_fin1 π E F) (p 1)
theorem
has_fpower_series_on_ball.differentiable_on
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{r : ennreal}
{f : E β F}
{x : E}
[complete_space F]
(h : has_fpower_series_on_ball f p x r) :
differentiable_on π f (emetric.ball x r)
theorem
analytic_on.differentiable_on
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(h : analytic_on π f s) :
differentiable_on π f s
theorem
has_fpower_series_on_ball.has_fderiv_at
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{r : ennreal}
{f : E β F}
{x : E}
[complete_space F]
(h : has_fpower_series_on_ball f p x r)
{y : E}
(hy : ββyββ < r) :
has_fderiv_at f (β(continuous_multilinear_curry_fin1 π E F) (p.change_origin y 1)) (x + y)
theorem
has_fpower_series_on_ball.fderiv_eq
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{r : ennreal}
{f : E β F}
{x : E}
[complete_space F]
(h : has_fpower_series_on_ball f p x r)
{y : E}
(hy : ββyββ < r) :
fderiv π f (x + y) = β(continuous_multilinear_curry_fin1 π E F) (p.change_origin y 1)
theorem
has_fpower_series_on_ball.fderiv
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{r : ennreal}
{f : E β F}
{x : E}
[complete_space F]
(h : has_fpower_series_on_ball f p x r) :
has_fpower_series_on_ball (fderiv π f) (β(continuous_multilinear_curry_fin1 π E F).comp_formal_multilinear_series (p.change_origin_series 1)) x r
If a function has a power series on a ball, then so does its derivative.
theorem
analytic_on.fderiv
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{s : set E}
[complete_space F]
(h : analytic_on π f s) :
analytic_on π (fderiv π f) s
If a function is analytic on a set s, so is its FrΓ©chet derivative.
theorem
analytic_on.iterated_fderiv
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{s : set E}
[complete_space F]
(h : analytic_on π f s)
(n : β) :
analytic_on π (iterated_fderiv π n f) s
If a function is analytic on a set s, so are its successive FrΓ©chet derivative.
theorem
analytic_on.cont_diff_on
{π : Type u_1}
[nontrivially_normed_field π]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : E β F}
{s : set E}
[complete_space F]
(h : analytic_on π f s)
{n : ββ} :
cont_diff_on π n f s
An analytic function is infinitely differentiable.
@[protected]
theorem
has_fpower_series_at.has_strict_deriv_at
{π : Type u_1}
[nontrivially_normed_field π]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π π F}
{f : π β F}
{x : π}
(h : has_fpower_series_at f p x) :
has_strict_deriv_at f (β(p 1) (Ξ» (_x : fin 1), 1)) x
@[protected]
theorem
has_fpower_series_at.has_deriv_at
{π : Type u_1}
[nontrivially_normed_field π]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π π F}
{f : π β F}
{x : π}
(h : has_fpower_series_at f p x) :
has_deriv_at f (β(p 1) (Ξ» (_x : fin 1), 1)) x
@[protected]
theorem
has_fpower_series_at.deriv
{π : Type u_1}
[nontrivially_normed_field π]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{p : formal_multilinear_series π π F}
{f : π β F}
{x : π}
(h : has_fpower_series_at f p x) :
theorem
analytic_on.deriv
{π : Type u_1}
[nontrivially_normed_field π]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{s : set π}
[complete_space F]
(h : analytic_on π f s) :
analytic_on π (deriv f) s
If a function is analytic on a set s, so is its derivative.
theorem
analytic_on.iterated_deriv
{π : Type u_1}
[nontrivially_normed_field π]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{s : set π}
[complete_space F]
(h : analytic_on π f s)
(n : β) :
analytic_on π (deriv^[n] f) s
If a function is analytic on a set s, so are its successive derivatives.