# mathlib3documentation

analysis.calculus.fderiv_analytic

# 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} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {f : E F} {x : E} (h : x) :
( (p 1)) x
theorem has_fpower_series_at.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {f : E F} {x : E} (h : x) :
( (p 1)) x
theorem has_fpower_series_at.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {f : E F} {x : E} (h : x) :
x
theorem analytic_at.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} :
f x x
theorem analytic_at.differentiable_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : f x) :
x
theorem has_fpower_series_at.fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {f : E F} {x : E} (h : x) :
f x = (p 1)
theorem has_fpower_series_on_ball.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {r : ennreal} {f : E F} {x : E} (h : r) :
r)
theorem analytic_on.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : f s) :
s
theorem has_fpower_series_on_ball.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {r : ennreal} {f : E F} {x : E} (h : r) {y : E} (hy : y‖₊ < r) :
( (p.change_origin y 1)) (x + y)
theorem has_fpower_series_on_ball.fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {r : ennreal} {f : E F} {x : E} (h : r) {y : E} (hy : y‖₊ < r) :
f (x + y) = (p.change_origin y 1)
theorem has_fpower_series_on_ball.fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {p : F} {r : ennreal} {f : E F} {x : E} (h : r) :
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} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : f s) :
(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} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : f s) (n : ) :
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} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : f s) {n : ℕ∞} :
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} [ 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} [ 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} [ 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} [ F] {f : 𝕜 F} {s : set 𝕜} (h : f s) :
(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} [ F] {f : 𝕜 F} {s : set 𝕜} (h : f s) (n : ) :
(deriv^[n] f) s

If a function is analytic on a set s, so are its successive derivatives.