mathlib documentation

analysis.calculus.fderiv_analytic

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) :
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) :
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) :
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) :
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) :
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) :

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) :
deriv f x = ⇑(p 1) (Ξ» (_x : fin 1), 1)
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.