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.

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.

def IsSymmSndFDerivWithinAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E) : Prop

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

def IsSymmSndFDerivAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : Prop

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

• IsSymmSndFDerivAt 𝕜 f x = ∀ (v w : E), ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) w) v

theorem IsSymmSndFDerivWithinAt.eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (h : IsSymmSndFDerivWithinAt 𝕜 f s x) (v w : E) : ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v

theorem IsSymmSndFDerivAt.eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : IsSymmSndFDerivAt 𝕜 f x) (v w : E) : ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) w) v

theorem fderivWithin_fderivWithin_eq_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : t ∈ nhdsWithin x s) (hf : ContDiffWithinAt 𝕜 2 f t x) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

theorem fderivWithin_fderivWithin_eq_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : s =ᶠ[nhds x] t) : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

theorem fderivWithin_fderivWithin_eq_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : s ∈ nhds x) : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderiv 𝕜 (fderiv 𝕜 f) x

@[simp]

theorem isSymmSndFDerivWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} : IsSymmSndFDerivWithinAt 𝕜 f Set.univ x ↔ IsSymmSndFDerivAt 𝕜 f x

theorem IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : IsSymmSndFDerivWithinAt 𝕜 f t x) (hst : t ∈ nhdsWithin x s) (hf : ContDiffWithinAt 𝕜 2 f t x) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) : IsSymmSndFDerivWithinAt 𝕜 f s x

theorem IsSymmSndFDerivWithinAt.congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : IsSymmSndFDerivWithinAt 𝕜 f s x) (hst : s =ᶠ[nhds x] t) : IsSymmSndFDerivWithinAt 𝕜 f t x

theorem isSymmSndFDerivWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (hst : s =ᶠ[nhds x] t) : IsSymmSndFDerivWithinAt 𝕜 f s x ↔ IsSymmSndFDerivWithinAt 𝕜 f t x

theorem IsSymmSndFDerivAt.isSymmSndFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (h : IsSymmSndFDerivAt 𝕜 f x) (hf : ContDiffAt 𝕜 2 f x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : IsSymmSndFDerivWithinAt 𝕜 f s x

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 : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F} (hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x) {x : E} (xs : x ∈ s) (hx : HasFDerivWithinAt f' f'' (interior s) x) {v 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 : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F} (hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x) {x : E} (xs : x ∈ s) (hx : HasFDerivWithinAt f' f'' (interior s) x) {v 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 : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F} (hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x) {x : E} (xs : x ∈ s) (hx : HasFDerivWithinAt 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ 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 ∈ interior s, HasFDerivAt f (f' x) x) {x : E} (xs : x ∈ s) (hx : HasFDerivWithinAt 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_of_real {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} {f : E → F} {f' : E → E →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 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. Version over ℝ. See second_derivative_symmetric_of_eventually for a version over ℝ or ℂ.

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

theorem second_derivative_symmetric {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E → E →L[𝕜] F} {f'' : E →L[𝕜] E →L[𝕜] F} {x : E} (hf : ∀ (y : E), HasFDerivAt f (f' y) y) (hx : HasFDerivAt 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.

theorem ContDiffAt.isSymmSndFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ∞} (hf : ContDiffAt 𝕜 n f x) (hn : 2 ≤ n) : IsSymmSndFDerivAt 𝕜 f x

If a function is C^2 at a point, then its second derivative there is symmetric.

theorem ContDiffWithinAt.isSymmSndFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hn : 2 ≤ n) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ closure (interior s)) (h'x : x ∈ s) : IsSymmSndFDerivWithinAt 𝕜 f s x

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.