Documentation

Mathlib.Analysis.Calculus.FDeriv.Symmetric

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.

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.

theorem Convex.taylor_approx_two_segment {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {s : Set E} (s_conv : Convex s) {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : xinterior s, HasFDerivAt f (f' x) x) {x : E} (xs : x s) (hx : HasFDerivWithinAt f' f'' (interior s) x) {v : E} {w : E} (hv : x + v interior s) (hw : x + v + w interior s) :
(fun (h : ) => f (x + h v + h w) - f (x + h v) - h (f' x) w - h ^ 2 (f'' v) w - (h ^ 2 / 2) (f'' w) w) =o[nhdsWithin 0 (Set.Ioi 0)] fun (h : ) => h ^ 2

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.

theorem Convex.isLittleO_alternate_sum_square {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {s : Set E} (s_conv : Convex s) {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : xinterior s, HasFDerivAt f (f' x) x) {x : E} (xs : x s) (hx : HasFDerivWithinAt f' f'' (interior s) x) {v : E} {w : E} (h4v : x + 4 v interior s) (h4w : x + 4 w interior s) :
(fun (h : ) => f (x + h (2 v + 2 w)) + f (x + h (v + w)) - f (x + h (2 v + w)) - f (x + h (v + 2 w)) - h ^ 2 (f'' v) w) =o[nhdsWithin 0 (Set.Ioi 0)] fun (h : ) => h ^ 2

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.

theorem Convex.second_derivative_within_at_symmetric_of_mem_interior {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {s : Set E} (s_conv : Convex s) {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : xinterior s, HasFDerivAt f (f' x) x) {x : E} (xs : x s) (hx : HasFDerivWithinAt f' f'' (interior s) x) {v : E} {w : E} (h4v : x + 4 v interior s) (h4w : x + 4 w interior s) :
(f'' w) v = (f'' v) 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.

theorem Convex.second_derivative_within_at_symmetric {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {s : Set E} (s_conv : Convex s) (hne : (interior s).Nonempty) {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : xinterior s, HasFDerivAt f (f' x) x) {x : E} (xs : x s) (hx : HasFDerivWithinAt f' f'' (interior s) x) (v : E) (w : E) :
(f'' v) w = (f'' w) v

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.

theorem second_derivative_symmetric_of_eventually {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {x : E} {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : ∀ᶠ (y : E) in nhds x, HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x) (v : E) (w : E) :
(f'' v) w = (f'' w) v

If a function is differentiable around x, and has two derivatives at x, then the second derivative is symmetric.

theorem second_derivative_symmetric {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {x : E} {f : EF} {f' : EE →L[] F} {f'' : E →L[] E →L[] F} (hf : ∀ (y : E), HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x) (v : E) (w : E) :
(f'' v) w = (f'' w) v

If a function is differentiable, and has two derivatives at x, then the second derivative is symmetric.