Frechet derivatives of analytic functions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.