Hessian is positive-semidefinite at a local minimizer

This is the Hessian positive-semidefiniteness criterion at a local minimizer.

Let $d$ be a natural number, let $f : \mathrm{EuclideanSpace}(\mathbb{R}, \mathrm{Fin}\,d) \to \mathbb{R}$ be twice continuously differentiable, and suppose $f$ attains a local minimum at $x_0$. Then for every direction $v$, the Hessian quadratic form is nonnegative:

Equivalently, the Hessian of $f$ at a local minimizer is a positive-semidefinite bilinear form. This is the key analytic input to maximum-principle arguments for second-order elliptic operators: at an interior minimum, the gradient vanishes and the second-order term has a sign, which is exactly what lets the operator inequality go through.

Formalization Note Lean has no separate Hessian matrix here; the quadratic form $\langle D^2 f(x_0) v, v \rangle$ is expressed as (fderiv ℝ (fun y => fderiv ℝ f y v) x₀) v, the derivative at $x_0$ in direction $v$ of the directional-derivative map $y \mapsto Df(y)(v)$.