Second-order necessary condition for a one-variable local minimum

This is the one-variable second-order necessary condition for a local minimum.

Let $g : \mathbb{R} \to \mathbb{R}$ be everywhere differentiable, suppose its derivative $g'$ is differentiable at the origin, and suppose $g$ attains a local minimum at $0$. Then

In words, the second derivative at a interior local minimizer cannot be strictly negative: otherwise the function would lie strictly below its value at the minimizer on one side. This is the converse direction of the usual second-derivative test, and it is the analytic core used to deduce Hessian positive-semidefiniteness at minimizers of several-variable functions by restriction to lines.

Formalization Note Lean's deriv is defined to be $0$ where the function is not differentiable, so the hypothesis that deriv g is differentiable at $0$ carries real content: it forces $g$ to be differentiable near $0$.