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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : formal_multilinear_series π E F}
{r : ββ₯0β}
{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)
@[protected]
theorem
has_fpower_series_at.has_strict_deriv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field π]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : formal_multilinear_series π π F}
{f : π β F}
{x : π}
(h : has_fpower_series_at f p x) :