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