Commit 2023-06-03 08:02 77a69e8c

View on Github →

feat: port Analysis.Calculus.FDerivSymmetric (#4616)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FDerivSymmetric.lean

added theorem Convex.isLittleO_alternate_sum_square

added theorem Convex.second_derivative_within_at_symmetric

added theorem Convex.second_derivative_within_at_symmetric_of_mem_interior

added theorem Convex.taylor_approx_two_segment

added theorem second_derivative_symmetric

added theorem second_derivative_symmetric_of_eventually