# mathlibdocumentation

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} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {f : E β F} {x : E} (h : x) :
(β F) (p 1)) x
theorem has_fpower_series_at.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {f : E β F} {x : E} (h : x) :
(β F) (p 1)) x
theorem has_fpower_series_at.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {f : E β F} {x : E} (h : x) :
f x
theorem analytic_at.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} :
analytic_at π f x β f x
theorem analytic_at.differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : analytic_at π f x) :
f s x
theorem has_fpower_series_at.fderiv_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {f : E β F} {x : E} (h : x) :
fderiv π f x = β F) (p 1)
theorem has_fpower_series_on_ball.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {r : ennreal} {f : E β F} {x : E} (h : r) :
f r)
theorem analytic_on.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (h : analytic_on π f s) :
f s
theorem has_fpower_series_on_ball.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {r : ennreal} {f : E β F} {x : E} (h : r) {y : E} (hy : ββ₯yβ₯β < r) :
(β F) (p.change_origin y 1)) (x + y)
theorem has_fpower_series_on_ball.fderiv_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {r : ennreal} {f : E β F} {x : E} (h : r) {y : E} (hy : ββ₯yβ₯β < r) :
fderiv π f (x + y) = β F) (p.change_origin y 1)
theorem has_fpower_series_on_ball.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : F} {r : ennreal} {f : E β F} {x : E} (h : r) :

If a function has a power series on a ball, then so does its derivative.

theorem analytic_on.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (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} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (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} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (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} {F : Type u_3} [normed_space π F] {p : π F} {f : π β F} {x : π} (h : x) :
(β(p 1) (Ξ» (_x : fin 1), 1)) x
@[protected]
theorem has_fpower_series_at.has_deriv_at {π : Type u_1} {F : Type u_3} [normed_space π F] {p : π F} {f : π β F} {x : π} (h : x) :
(β(p 1) (Ξ» (_x : fin 1), 1)) x
@[protected]
theorem has_fpower_series_at.deriv {π : Type u_1} {F : Type u_3} [normed_space π F] {p : π F} {f : π β F} {x : π} (h : x) :
x = β(p 1) (Ξ» (_x : fin 1), 1)
theorem analytic_on.deriv {π : Type u_1} {F : Type u_3} [normed_space π F] {f : π β F} {s : set π} (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} {F : Type u_3} [normed_space π F] {f : π β F} {s : set π} (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.