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
HasFPowerSeriesAt.hasStrictFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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) (FormalMultilinearSeries.changeOrigin p y 1)) (x + y)
theorem
HasFPowerSeriesOnBall.fderiv_eq
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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) (FormalMultilinearSeries.changeOrigin p y 1)
theorem
HasFPowerSeriesOnBall.fderiv
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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)
(ContinuousLinearMap.compFormalMultilinearSeries
(β(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 π E F).toLinearEquiv))
(FormalMultilinearSeries.changeOriginSeries p 1))
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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[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 u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{p : FormalMultilinearSeries π π F}
{f : π β F}
{x : π}
(h : HasFPowerSeriesAt f p x)
:
HasStrictDerivAt f (β(p 1) fun x => 1) x
theorem
HasFPowerSeriesAt.hasDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{p : FormalMultilinearSeries π π F}
{f : π β F}
{x : π}
(h : HasFPowerSeriesAt f p x)
:
HasDerivAt f (β(p 1) fun x => 1) x
theorem
HasFPowerSeriesAt.deriv
{π : Type u_1}
[NontriviallyNormedField π]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{p : FormalMultilinearSeries π π F}
{f : π β F}
{x : π}
(h : HasFPowerSeriesAt f p x)
:
theorem
AnalyticOn.deriv
{π : Type u_1}
[NontriviallyNormedField π]
{F : Type u_3}
[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 u_3}
[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.