Theorem Convex.isLittleO_alternate_sum_square

Modification history

2023-06-03 08:02
Mathlib/Analysis/Calculus/FDerivSymmetric.lean
feat: port Analysis.Calculus.FDerivSymmetric (#4616)
Added Convex.isLittleO_alternate_sum_squareView on Github →