Symmetry of the second derivative #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.is_o_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.
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.
If a function is differentiable, and has two derivatives at x, then the second
derivative is symmetric.