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