mathlib

ed377e13 - feat(analysis/convex): a local minimum of a convex function is a global minimum (#3613)

feat(analysis/convex): a local minimum of a convex function is a global minimum (#3613) Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr>