One-dimensional iterated derivatives
We define the n-th derivative of a function f : π β F as a function
iterated_deriv n f : π β F, as well as a version on domains iterated_deriv_within n f s : π β F,
and prove their basic properties.
Main definitions and results
Let π be a nondiscrete normed field, and F a normed vector space over π. Let f : π β F.
iterated_deriv n fis then-th derivative off, seen as a function fromπtoF. It is defined as then-th FrΓ©chet derivative (which is a multilinear map) applied to the vector(1, ..., 1), to take advantage of all the existing framework, but we show that it coincides with the naive iterative definition.iterated_deriv_eq_iteratestates that then-th derivative offis obtained by starting fromfand differentiating itntimes.iterated_deriv_within n f sis then-th derivative offwithin the domains. It only behaves well whenshas the unique derivative property.iterated_deriv_within_eq_iteratestates that then-th derivative offin the domainsis obtained by starting fromfand differentiating itntimes withins. This only holds whenshas the unique derivative property.
Implementation details
The results are deduced from the corresponding results for the more general (multilinear) iterated
FrΓ©chet derivative. For this, we write iterated_deriv n f as the composition of
iterated_fderiv π n f and a continuous linear equiv. As continuous linear equivs respect
differentiability and commute with differentiation, this makes it possible to prove readily that
the derivative of the n-th derivative is the n+1-th derivative in iterated_deriv_within_succ,
by translating the corresponding result iterated_fderiv_within_succ_apply_left for the
iterated FrΓ©chet derivative.
The n-th iterated derivative of a function from π to F, as a function from π to F.
Equations
- iterated_deriv n f x = β(iterated_fderiv π n f x) (Ξ» (i : fin n), 1)
The n-th iterated derivative of a function from π to F within a set s, as a function
from π to F.
Equations
- iterated_deriv_within n f s x = β(iterated_fderiv_within π n f s x) (Ξ» (i : fin n), 1)
Properties of the iterated derivative within a set
Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative
Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.
The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative
multiplied by the product of the m is.
If the first n derivatives within a set of a function are continuous, and its first n-1
derivatives are differentiable, then the function is C^n. This is not an equivalence in general,
but this is an equivalence when the set has unique derivatives, see
times_cont_diff_on_iff_continuous_on_differentiable_on_deriv.
To check that a function is n times continuously differentiable, it suffices to check that its
first n derivatives are differentiable. This is slightly too strong as the condition we
require on the n-th derivative is differentiability instead of continuity, but it has the
advantage of avoiding the discussion of continuity in the proof (and for n = β this is optimal).
On a set with unique derivatives, a C^n function has derivatives up to n which are
continuous.
On a set with unique derivatives, a C^n function has derivatives less than n which are
differentiable.
The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be
reformulated in terms of the one-dimensional derivative on sets with unique derivatives.
The n+1-th iterated derivative within a set with unique derivatives can be obtained by
differentiating the n-th iterated derivative.
The n-th iterated derivative within a set with unique derivatives can be obtained by
iterating n times the differentiation operation.
The n+1-th iterated derivative within a set with unique derivatives can be obtained by
taking the n-th derivative of the derivative.
Properties of the iterated derivative on the whole space
Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative
Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.
The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative
multiplied by the product of the m is.
The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be
reformulated in terms of the one-dimensional derivative.
To check that a function is n times continuously differentiable, it suffices to check that its
first n derivatives are differentiable. This is slightly too strong as the condition we
require on the n-th derivative is differentiability instead of continuity, but it has the
advantage of avoiding the discussion of continuity in the proof (and for n = β this is optimal).
The n+1-th iterated derivative can be obtained by differentiating the n-th
iterated derivative.
The n-th iterated derivative can be obtained by iterating n times the
differentiation operation.
The n+1-th iterated derivative can be obtained by taking the n-th derivative of the
derivative.