# 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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} (h : ) :
HasStrictFDerivAt f (() (p 1)) x
theorem HasFPowerSeriesAt.hasFDerivAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} (h : ) :
HasFDerivAt f (() (p 1)) x
theorem HasFPowerSeriesAt.differentiableAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} (h : ) :
DifferentiableAt π f x
theorem AnalyticAt.differentiableAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {x : E} :
AnalyticAt π f x β DifferentiableAt π f x
theorem AnalyticAt.differentiableWithinAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} (h : ) :
fderiv π f x = () (p 1)
theorem HasFPowerSeriesOnBall.differentiableOn {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {f : E β F} {x : E} [] (h : ) :
DifferentiableOn π f ()
theorem AnalyticOn.differentiableOn {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {s : Set E} (h : AnalyticOn π f s) :
DifferentiableOn π f s
theorem HasFPowerSeriesOnBall.hasFDerivAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {f : E β F} {x : E} [] (h : ) {y : E} (hy : β < r) :
HasFDerivAt f (() (p.changeOrigin y 1)) (x + y)
theorem HasFPowerSeriesOnBall.fderiv_eq {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {f : E β F} {x : E} [] (h : ) {y : E} (hy : β < r) :
fderiv π f (x + y) = () (p.changeOrigin y 1)
theorem HasFPowerSeriesOnBall.fderiv {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {f : E β F} {x : E} [] (h : ) :
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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {s : Set E} [] (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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {s : Set E} [] (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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {s : Set E} [] (h : AnalyticOn π f s) {n : ββ} :
ContDiffOn π n f s

An analytic function is infinitely differentiable.

theorem AnalyticAt.contDiffAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {x : E} [] (h : AnalyticAt π f x) {n : ββ} :
ContDiffAt π n f x
theorem HasFPowerSeriesAt.hasStrictDerivAt {π : Type u_1} [] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π π F} {f : π β F} {x : π} (h : ) :
HasStrictDerivAt f ((p 1) fun (x : Fin 1) => 1) x
theorem HasFPowerSeriesAt.hasDerivAt {π : Type u_1} [] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π π F} {f : π β F} {x : π} (h : ) :
HasDerivAt f ((p 1) fun (x : Fin 1) => 1) x
theorem HasFPowerSeriesAt.deriv {π : Type u_1} [] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π π F} {f : π β F} {x : π} (h : ) :
deriv f x = (p 1) fun (x : Fin 1) => 1
theorem AnalyticOn.deriv {π : Type u_1} [] {F : Type v} [NormedSpace π F] {f : π β F} {s : Set π} [] (h : AnalyticOn π f s) :
AnalyticOn π () s

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

theorem AnalyticOn.iterated_deriv {π : Type u_1} [] {F : Type v} [NormedSpace π F] {f : π β F} {s : Set π} [] (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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {n : β} {f : E β F} {x : E} (h : ) :
DifferentiableOn π f ()
theorem HasFiniteFPowerSeriesOnBall.hasFDerivAt {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {n : β} {f : E β F} {x : E} (h : ) {y : E} (hy : β < r) :
HasFDerivAt f (() (p.changeOrigin y 1)) (x + y)
theorem HasFiniteFPowerSeriesOnBall.fderiv_eq {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {n : β} {f : E β F} {x : E} (h : ) {y : E} (hy : β < r) :
fderiv π f (x + y) = () (p.changeOrigin y 1)
theorem HasFiniteFPowerSeriesOnBall.fderiv {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {r : ENNReal} {n : β} {f : E β F} {x : E} (h : ) :
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} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {f : E β F} {x : E} (h : CPolynomialAt π f x) {n : ββ} :
ContDiffAt π n f x
theorem CPolynomialOn.deriv {π : Type u_1} [] {F : Type v} [NormedSpace π F] {f : π β F} {s : Set π} (h : CPolynomialOn π f s) :
CPolynomialOn π () s

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

theorem CPolynomialOn.iterated_deriv {π : Type u_1} [] {F : Type v} [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} [] {F : Type v} [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 ( + 1) β€
theorem ContinuousMultilinearMap.changeOriginSeries_support {π : Type u_1} [] {F : Type v} [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 β  ) :
f.toFormalMultilinearSeries.changeOriginSeries k l = 0
theorem ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries {π : Type u_1} [] {F : Type v} [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) [] :
(continuousMultilinearCurryFin1 π ((i : ΞΉ) β E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x
theorem ContinuousMultilinearMap.hasFDerivAt {π : Type u_1} [] {F : Type v} [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) [] :
HasFDerivAt (βf) (f.linearDeriv x) x
theorem ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv {π : Type u_1} [] {F : Type v} [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} [] {F : Type v} [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} [] {F : Type v} [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β β€ β(().descFactorial n) * * ^ ( - n)
theorem ContinuousMultilinearMap.cPolynomialAt {π : Type u_1} [] {F : Type v} [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} [] {F : Type v} [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} [] {F : Type v} [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} [] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} {r : ENNReal} (h : ) :
iteratedFDeriv π 0 f x = p 0
theorem HasFPowerSeriesOnBall.factorial_smul {π : Type u_1} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} {r : ENNReal} (h : ) (y : E) [] (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} [] {E : Type u} [NormedSpace π E] {F : Type v} [NormedSpace π F] {p : FormalMultilinearSeries π E F} {f : E β F} {x : E} {r : ENNReal} (h : ) [] [CharZero π] {y : E} (hy : y β ) :
HasSum (fun (n : β) => (βn.factorial)β»ΒΉ β’ (iteratedFDeriv π n f x) fun (x : Fin n) => y) (f (x + y))