Iterated derivatives of a function #
In this file, we define iteratively the n+1-th derivative of a function as the
derivative of the n-th derivative. It is called iteratedFDeriv π n f x where π is the
field, n is the number of iterations, f is the function and x is the point, and it is given
as an n-multilinear map. We also define a version iteratedFDerivWithin relative to a domain.
Note that, in domains, there may be several choices of possible derivative, so we make some
arbitrary choice in the definition.
We also define a predicate HasFTaylorSeriesUpTo (and its localized version
HasFTaylorSeriesUpToOn), saying that a sequence of multilinear maps is a sequence of
derivatives of f. Contrary to iteratedFDerivWithin, it accommodates well the
non-uniqueness of derivatives.
Main definitions and results #
Let f : E β F be a map between normed vector spaces over a nontrivially normed field π.
HasFTaylorSeriesUpTo n f p: expresses that the formal multilinear seriespis a sequence of iterated derivatives off, up to then-th term (wherenis a natural number orβ).HasFTaylorSeriesUpToOn n f p s: same thing, but inside a sets. The notion of derivative is now taken insides. In particular, derivatives don't have to be unique.iteratedFDerivWithin π n f s xis ann-th derivative offover the fieldπon the setsat the pointx. It is a continuous multilinear map fromE^ntoF, defined as a derivative withinsofiteratedFDerivWithin π (n-1) f sif one exists, and0otherwise.iteratedFDeriv π n f xis then-th derivative offover the fieldπat the pointx. It is a continuous multilinear map fromE^ntoF, defined as a derivative ofiteratedFDeriv π (n-1) fif one exists, and0otherwise.
Side of the composition, and universe issues #
With a naΓ―ve direct definition, the n-th derivative of a function belongs to the space
E βL[π] (E βL[π] (E ... F)...))) where there are n iterations of E βL[π]. This space
may also be seen as the space of continuous multilinear functions on n copies of E with
values in F, by uncurrying. This is the point of view that is usually adopted in textbooks,
and that we also use. This means that the definition and the first proofs are slightly involved,
as one has to keep track of the uncurrying operation. The uncurrying can be done from the
left or from the right, amounting to defining the n+1-th derivative either as the derivative of
the n-th derivative, or as the n-th derivative of the derivative.
For proofs, it would be more convenient to use the latter approach (from the right),
as it means to prove things at the n+1-th step we only need to understand well enough the
derivative in E βL[π] F (contrary to the approach from the left, where one would need to know
enough on the n-th derivative to deduce things on the n+1-th derivative).
However, the definition from the right leads to a universe polymorphism problem: if we define
iteratedFDeriv π (n + 1) f x = iteratedFDeriv π n (fderiv π f) x by induction, we need to
generalize over all spaces (as f and fderiv π f don't take values in the same space). It is
only possible to generalize over all spaces in some fixed universe in an inductive definition.
For f : E β F, then fderiv π f is a map E β (E βL[π] F). Therefore, the definition will only
work if F and E βL[π] F are in the same universe.
This issue does not appear with the definition from the left, where one does not need to generalize
over all spaces. Therefore, we use the definition from the left. This means some proofs later on
become a little bit more complicated: to prove that a function is C^n, the most efficient approach
is to exhibit a formula for its n-th derivative and prove it is continuous (contrary to the
inductive approach where one would prove smoothness statements without giving a formula for the
derivative). In the end, this approach is still satisfactory as it is good to have formulas for the
iterated derivatives in various constructions.
One point where we depart from this explicit approach is in the proof of smoothness of a
composition: there is a formula for the n-th derivative of a composition (FaΓ di Bruno's formula),
but it is very complicated and barely usable, while the inductive proof is very simple. Thus, we
give the inductive proof. As explained above, it works by generalizing over the target space, hence
it only works well if all spaces belong to the same universe. To get the general version, we lift
things to a common universe using a trick.
Variables management #
The textbook definitions and proofs use various identifications and abuse of notations, for instance
when saying that the natural space in which the derivative lives, i.e.,
E βL[π] (E βL[π] ( ... βL[π] F)), is the same as a space of multilinear maps. When doing things
formally, we need to provide explicit maps for these identifications, and chase some diagrams to see
everything is compatible with the identifications. In particular, one needs to check that taking the
derivative and then doing the identification, or first doing the identification and then taking the
derivative, gives the same result. The key point for this is that taking the derivative commutes
with continuous linear equivalences. Therefore, we need to implement all our identifications with
continuous linear equivs.
Notations #
We use the notation E [Γn]βL[π] F for the space of continuous multilinear maps on E^n with
values in F. This is the space in which the n-th derivative of a function from E to F lives.
In this file, we denote β€ : ββ with β.
Functions with a Taylor series on a domain #
HasFTaylorSeriesUpToOn n f p s registers the fact that p 0 = f and p (m+1) is a
derivative of p m for m < n, and is continuous for m β€ n. This is a predicate analogous to
HasFDerivWithinAt but for higher order derivatives.
Notice that p does not sum up to f on the diagonal (FormalMultilinearSeries.sum), even if
f is analytic and n = β: an additional 1/m! factor on the mth term is necessary for that.
- zero_eq : β x β s, (p x 0).curry0 = f x
- fderivWithin : β (m : β), ββm < n β β x β s, HasFDerivWithinAt (fun (x : E) => p x m) (p x m.succ).curryLeft s x
- cont : β (m : β), βm β€ n β ContinuousOn (fun (x : E) => p x m) s
Instances For
If two functions coincide on a set s, then a Taylor series for the first one is as well a
Taylor series for the second one.
In the case that n = β we don't need the continuity assumption in
HasFTaylorSeriesUpToOn.
If a function has a Taylor series at order at least 1, then the term of order 1 of this
series is a derivative of f.
If a function has a Taylor series at order at least 1 on a neighborhood of x, then the term
of order 1 of this series is a derivative of f at x.
If a function has a Taylor series at order at least 1 on a neighborhood of x, then
in a neighborhood of x, the term of order 1 of this series is a derivative of f.
If a function has a Taylor series at order at least 1 on a neighborhood of x, then
it is differentiable at x.
p is a Taylor series of f up to n+1 if and only if p is a Taylor series up to n, and
p (n + 1) is a derivative of p n.
p is a Taylor series of f up to n+1 if and only if p.shift is a Taylor series up to n
for p 1, which is a derivative of f. Version for n : β.
p is a Taylor series of f up to β€ if and only if p.shift is a Taylor series up to β€
for p 1, which is a derivative of f.
p is a Taylor series of f up to n+1 if and only if p.shift is a Taylor series up to n
for p 1, which is a derivative of f. Version for n : WithTop ββ.
Iterated derivative within a set #
The n-th derivative of a function along a set, defined inductively by saying that the n+1-th
derivative of f is the derivative of the n-th derivative of f along this set, together with
an uncurrying step to see it as a multilinear map in n+1 variables..
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formal Taylor series associated to a function within a set.
Equations
- ftaylorSeriesWithin π f s x n = iteratedFDerivWithin π n f s x
Instances For
Writing explicitly the n+1-th derivative as the composition of a currying linear equiv,
and the derivative of the n-th derivative.
Writing explicitly the n+1-th derivative as the composition of a currying linear equiv,
and the n-th derivative of the derivative.
On a set of unique differentiability, the second derivative is obtained by taking the derivative of the derivative.
If two functions coincide in a neighborhood of x within a set s and at x, then their
iterated differentials within this set at x coincide.
If two functions coincide on a set s, then their iterated differentials within this set
coincide. See also Filter.EventuallyEq.iteratedFDerivWithin_eq and
Filter.EventuallyEq.iteratedFDerivWithin.
If two functions coincide on a set s, then their iterated differentials within this set
coincide. See also Filter.EventuallyEq.iteratedFDerivWithin_eq and
Filter.EventuallyEq.iteratedFDerivWithin.
The iterated differential within a set s at a point x is not modified if one intersects
s with a neighborhood of x within s.
The iterated differential within a set s at a point x is not modified if one intersects
s with a neighborhood of x.
The iterated differential within a set s at a point x is not modified if one intersects
s with an open set containing x.
On a set with unique differentiability, any choice of iterated differential has to coincide
with the one we have chosen in iteratedFDerivWithin π m f s.
Alias of HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn.
On a set with unique differentiability, any choice of iterated differential has to coincide
with the one we have chosen in iteratedFDerivWithin π m f s.
Functions with a Taylor series on the whole space #
HasFTaylorSeriesUpTo n f p registers the fact that p 0 = f and p (m+1) is a
derivative of p m for m < n, and is continuous for m β€ n. This is a predicate analogous to
HasFDerivAt but for higher order derivatives.
Notice that p does not sum up to f on the diagonal (FormalMultilinearSeries.sum), even if
f is analytic and n = β: an addition 1/m! factor on the mth term is necessary for that.
- zero_eq : β (x : E), (p x 0).curry0 = f x
- fderiv : β (m : β), βm < n β β (x : E), HasFDerivAt (fun (y : E) => p y m) (p x m.succ).curryLeft x
- cont : β (m : β), βm β€ n β Continuous fun (x : E) => p x m
Instances For
Alias of HasFTaylorSeriesUpTo.of_le.
In the case that n = β we don't need the continuity assumption in
HasFTaylorSeriesUpTo.
If a function has a Taylor series at order at least 1, then the term of order 1 of this
series is a derivative of f.
p is a Taylor series of f up to n+1 if and only if p.shift is a Taylor series up to n
for p 1, which is a derivative of f.
Alias of hasFTaylorSeriesUpTo_succ_nat_iff_right.
p is a Taylor series of f up to n+1 if and only if p.shift is a Taylor series up to n
for p 1, which is a derivative of f.
Iterated derivative #
The n-th derivative of a function, as a multilinear map, defined inductively.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formal Taylor series associated to a function.
Equations
- ftaylorSeries π f x n = iteratedFDeriv π n f x
Instances For
Writing explicitly the n+1-th derivative as the composition of a currying linear equiv,
and the derivative of the n-th derivative.
Writing explicitly the derivative of the n-th derivative as the composition of a currying
linear equiv, and the n + 1-th derivative.
In an open set, the iterated derivative within this set coincides with the global iterated derivative.
Writing explicitly the n+1-th derivative as the composition of a currying linear equiv,
and the n-th derivative of the derivative.