mathlib documentation

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.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.

theorem convex.taylor_approx_two_segment {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {s : set E} (s_conv : convex s) {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ (x : E), x interior shas_fderiv_at f (f' x) x) {x : E} (xs : x s) (hx : has_fderiv_within_at f' f'' (interior s) x) {v w : E} (hv : x + v interior s) (hw : x + v + w interior s) :
asymptotics.is_o (λ (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) (λ (h : ), h ^ 2) (𝓝[set.Ioi 0] 0)

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.is_o_alternate_sum_square {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {s : set E} (s_conv : convex s) {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ (x : E), x interior shas_fderiv_at f (f' x) x) {x : E} (xs : x s) (hx : has_fderiv_within_at f' f'' (interior s) x) {v w : E} (h4v : x + 4 v interior s) (h4w : x + 4 w interior s) :
asymptotics.is_o (λ (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) (λ (h : ), h ^ 2) (𝓝[set.Ioi 0] 0)

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} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {s : set E} (s_conv : convex s) {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ (x : E), x interior shas_fderiv_at f (f' x) x) {x : E} (xs : x s) (hx : has_fderiv_within_at f' f'' (interior s) x) {v 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} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {s : set E} (s_conv : convex s) (hne : (interior s).nonempty) {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ (x : E), x interior shas_fderiv_at f (f' x) x) {x : E} (xs : x s) (hx : has_fderiv_within_at f' f'' (interior s) x) (v 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} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {x : E} {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ᶠ (y : E) in 𝓝 x, has_fderiv_at f (f' y) y) (hx : has_fderiv_at f' f'' x) (v 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} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {x : E} {f : E → F} {f' : E → (E →L[] F)} {f'' : E →L[] E →L[] F} (hf : ∀ (y : E), has_fderiv_at f (f' y) y) (hx : has_fderiv_at f' f'' x) (v 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.