mathlib

f5f8a20f - feat(analysis/calculus/fderiv_symmetric): prove that the second derivative is symmetric (#8104)

feat(analysis/calculus/fderiv_symmetric): prove that the second derivative is symmetric (#8104) We show that, if a function is differentiable over the reals around a point `x`, and is second-differentiable at `x`, then the second derivative is symmetric. In fact, we even prove a stronger statement for functions differentiable within a convex set, to be able to apply it for functions on the half-plane or the quadrant.