Symmetry of the second derivative #
We show that, over the reals, the second derivative is symmetric.
The most precise result is Convex.second_derivative_within_at_symmetric. It asserts that,
if a function is differentiable inside a convex set s with nonempty interior, and has a second
derivative within s at a point x, then this second derivative at x is symmetric. Note that
this result does not require continuity of the first derivative.
The following particular cases of this statement are especially relevant:
second_derivative_symmetric_of_eventually asserts that, if a function is differentiable on a
neighborhood of x, and has a second derivative at x, then this second derivative is symmetric.
second_derivative_symmetric asserts that, if a function is differentiable, and has a second
derivative at x, then this second derivative is symmetric.
There statements are given over โ or โ, the general version being deduced from the real
version. We also give statements in terms of fderiv and fderivWithin, called respectively
ContDiffAt.isSymmSndFDerivAt and ContDiffWithinAt.isSymmSndFDerivWithinAt (the latter
requiring that the point under consideration is accumulated by points in the interior of the set).
These are written using ad hoc predicates IsSymmSndFDerivAt and IsSymmSndFDerivWithinAt, which
increase readability of statements in differential geometry where they show up a lot.
We also deduce statements over an arbitrary field, requiring that the function is C^2 if the field
is โ or โ, and analytic otherwise. Formally, we assume that the function is C^n
with minSmoothness ๐ 2 โค n, where minSmoothness ๐ i is i if ๐ is โ or โ,
and ฯ otherwise.
Implementation note #
For the proof, we obtain an asymptotic expansion to order two of f (x + v + w) - f (x + v), by
using the mean value inequality applied to a suitable function along the
segment [x + v, x + v + w]. This expansion involves f'' โฌ w as we move along a segment directed
by w (see Convex.taylor_approx_two_segment).
Consider the alternate sum f (x + v + w) + f x - f (x + v) - f (x + w), corresponding to the
values of f along a rectangle based at x with sides v and w. One can write it using the two
sides directed by w, as (f (x + v + w) - f (x + v)) - (f (x + w) - f x). Together with the
previous asymptotic expansion, one deduces that it equals f'' v w + o(1) when v, w tends to 0.
Exchanging the roles of v and w, one instead gets an asymptotic expansion f'' w v, from which
the equality f'' v w = f'' w v follows.
In our most general statement, we only assume that f is differentiable inside a convex set s, so
a few modifications have to be made. Since we don't assume continuity of f at x, we consider
instead the rectangle based at x + v + w with sides v and w,
in Convex.isLittleO_alternate_sum_square, but the argument is essentially the same. It only works
when v and w both point towards the interior of s, to make sure that all the sides of the
rectangle are contained in s by convexity. The general case follows by linearity, though.
Definition recording that a function has a symmetric second derivative within a set at a point. This is automatic in most cases of interest (open sets over real or complex vector fields, or general case for analytic functions), but we can express theorems of calculus using this as a general assumption, and then specialize to these situations.
Equations
- IsSymmSndFDerivWithinAt ๐ f s x = โ (v w : E), ((fderivWithin ๐ (fderivWithin ๐ f s) s x) v) w = ((fderivWithin ๐ (fderivWithin ๐ f s) s x) w) v
Instances For
Definition recording that a function has a symmetric second derivative at a point. This is automatic in most cases of interest (open sets over real or complex vector fields, or general case for analytic functions), but we can express theorems of calculus using this as a general assumption, and then specialize to these situations.
Equations
Instances For
If a function is analytic within a set at a point, then its second derivative is symmetric.
If a function is analytic at a point, then its second derivative is symmetric.
Assume that f is differentiable inside a convex set s, and that its derivative f' is
differentiable at a point x. Then, given two vectors v and w pointing inside s, one can
Taylor-expand to order two the function f on the segment [x + h v, x + h (v + w)], giving a
bilinear estimate for f (x + hv + hw) - f (x + hv) in terms of f' w and of f'' โฌ w, up to
o(h^2).
This is a technical statement used to show that the second derivative is symmetric.
One can get f'' v w as the limit of h ^ (-2) times the alternate sum of the values of f
along the vertices of a quadrilateral with sides h v and h w based at x.
In a setting where f is not guaranteed to be continuous at f, we can still
get this if we use a quadrilateral based at h v + h w.
Assume that f is differentiable inside a convex set s, and that its derivative f' is
differentiable at a point x. Then, given two vectors v and w pointing inside s, one
has f'' v w = f'' w v. Superseded by Convex.second_derivative_within_at_symmetric, which
removes the assumption that v and w point inside s.
If a function is differentiable inside a convex set with nonempty interior, and has a second derivative at a point of this convex set, then this second derivative is symmetric.
If a function is differentiable around x, and has two derivatives at x, then the second
derivative is symmetric. Version over โ. See second_derivative_symmetric_of_eventually for a
version over โ or โ.
If a function is differentiable, and has two derivatives at x, then the second
derivative is symmetric.
minSmoothness ๐ n is the minimal smoothness exponent larger than or equal to n for which
one can do serious calculus in ๐. If ๐ is โ or โ, this is just n. Otherwise,
this is ฯ as only analytic functions are well behaved on โโ, say.
Equations
- minSmoothness ๐ n = if IsRCLikeNormedField ๐ then n else โค
Instances For
If minSmoothness ๐ m โค n for some (finite) integer m, then one can
find n' โ [minSmoothness ๐ m, n] which is not โ: over โ or โ, just take m, and otherwise
just take ฯ. The interest of this technical lemma is that, if a function is C^{n'} at a point
for n' โ โ, then it is C^{n'} on a neighborhood of the point (this property fails only
in C^โ smoothness, see ContDiffWithinAt.contDiffOn).
If a function is C^2 at a point, then its second derivative there is symmetric. Over a field
different from โ or โ, we should require that the function is analytic.
If a function is C^2 within a set at a point, and accumulated by points in the interior
of the set, then its second derivative there is symmetric. Over a field
different from โ or โ, we should require that the function is analytic.