Documentation

Mathlib.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.

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