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.

As an application, we show that continuous multilinear maps are smooth. We also compute their iterated derivatives, in ContinuousMultilinearMap.iteratedFDeriv_eq.

theorem HasFPowerSeriesAt.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) : HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

theorem HasFPowerSeriesAt.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) : HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

theorem HasFPowerSeriesAt.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) : DifferentiableAt 𝕜 f x

theorem AnalyticAt.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} : AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x

theorem AnalyticAt.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : AnalyticAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x

theorem HasFPowerSeriesAt.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) : fderiv 𝕜 f x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)

theorem HasFPowerSeriesOnBall.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r)

theorem AnalyticOn.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s

theorem HasFPowerSeriesOnBall.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : ↑‖y‖₊ < r) : HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)

theorem HasFPowerSeriesOnBall.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : ↑‖y‖₊ < r) : fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)

theorem HasFPowerSeriesOnBall.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r

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

theorem AnalyticOn.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (fderiv 𝕜 f) s

If a function is analytic on a set s, so is its Fréchet derivative.

theorem AnalyticOn.iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) : AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s

If a function is analytic on a set s, so are its successive Fréchet derivative.

theorem AnalyticOn.contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s

An analytic function is infinitely differentiable.

theorem AnalyticAt.contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} : ContDiffAt 𝕜 n f x

theorem HasFPowerSeriesAt.hasStrictDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) : HasStrictDerivAt f ((p 1) fun (x : Fin 1) => 1) x

theorem HasFPowerSeriesAt.hasDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) : HasDerivAt f ((p 1) fun (x : Fin 1) => 1) x

theorem HasFPowerSeriesAt.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) : deriv f x = (p 1) fun (x : Fin 1) => 1

theorem AnalyticOn.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (deriv f) s

If a function is analytic on a set s, so is its derivative.

theorem AnalyticOn.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) : AnalyticOn 𝕜 (deriv^[n] f) s

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

The case of continuously polynomial functions. We get the same differentiability results as for analytic functions, but without the assumptions that F is complete.

theorem HasFiniteFPowerSeriesOnBall.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) : DifferentiableOn 𝕜 f (EMetric.ball x r)

theorem HasFiniteFPowerSeriesOnBall.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : ↑‖y‖₊ < r) : HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)

theorem HasFiniteFPowerSeriesOnBall.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : ↑‖y‖₊ < r) : fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)

theorem HasFiniteFPowerSeriesOnBall.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r) : HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r

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

theorem HasFiniteFPowerSeriesOnBall.fderiv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) : HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r

If a function has a finite power series on a ball, then so does its derivative. This is a variant of HasFiniteFPowerSeriesOnBall.fderiv where the degree of f is < n and not < n + 1.

theorem CPolynomialOn.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (fderiv 𝕜 f) s

If a function is polynomial on a set s, so is its Fréchet derivative.

theorem CPolynomialOn.iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : CPolynomialOn 𝕜 f s) (n : ℕ) : CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s

If a function is polynomial on a set s, so are its successive Fréchet derivative.

theorem CPolynomialOn.contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : CPolynomialOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s

A polynomial function is infinitely differentiable.

theorem CPolynomialAt.contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) {n : ℕ∞} : ContDiffAt 𝕜 n f x

theorem CPolynomialOn.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (deriv f) s

If a function is polynomial on a set s, so is its derivative.

theorem CPolynomialOn.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : CPolynomialOn 𝕜 f s) (n : ℕ) : CPolynomialOn 𝕜 (deriv^[n] f) s

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

theorem ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) : HasFiniteFPowerSeriesOnBall (⇑f) f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤

theorem ContinuousMultilinearMap.changeOriginSeries_support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {k : ℕ} {l : ℕ} (h : k + l ≠ Fintype.card ι) : f.toFormalMultilinearSeries.changeOriginSeries k l = 0

theorem ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) [DecidableEq ι] : (continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x

theorem ContinuousMultilinearMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) [DecidableEq ι] : HasFDerivAt (⇑f) (f.linearDeriv x) x

theorem ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) : HasFTaylorSeriesUpTo ⊤ ⇑f fun (v : (i : ι) → E i) (n : ℕ) => f.iteratedFDeriv n v

A continuous multilinear function f admits a Taylor series, whose successive terms are given by f.iteratedFDeriv n. This is the point of the definition of f.iteratedFDeriv.

theorem ContinuousMultilinearMap.iteratedFDeriv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ) : iteratedFDeriv 𝕜 n ⇑f = f.iteratedFDeriv n

theorem ContinuousMultilinearMap.norm_iteratedFDeriv_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ) (x : (i : ι) → E i) : ‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

theorem ContinuousMultilinearMap.cPolynomialAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) : CPolynomialAt 𝕜 (⇑f) x

theorem ContinuousMultilinearMap.cPolyomialOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) : CPolynomialOn 𝕜 ⇑f ⊤

theorem ContinuousMultilinearMap.contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {n : ℕ∞} (x : (i : ι) → E i) : ContDiffAt 𝕜 n (⇑f) x

theorem ContinuousMultilinearMap.contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {n : ℕ∞} : ContDiff 𝕜 n ⇑f

theorem FormalMultilinearSeries.derivSeries_apply_diag {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (x : E) : ((p.derivSeries n) fun (x_1 : Fin n) => x) x = (n + 1) • (p (n + 1)) fun (x_1 : Fin (n + 1)) => x

theorem HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) : iteratedFDeriv 𝕜 0 f x = p 0

theorem HasFPowerSeriesOnBall.factorial_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) (y : E) [CompleteSpace F] (n : ℕ) : (n.factorial • (p n) fun (x : Fin n) => y) = (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => y

theorem HasFPowerSeriesOnBall.hasSum_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) [CompleteSpace F] [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0 r) : HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => y) (f (x + y))