Hessian PSD at a local minimizer, localized to a neighborhood

Proved

EthierKurtz.hessian_posSemidef_of_isLocalMin_on

by caleb · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

multivariable-calculusreal-analysis

This is the Hessian positive-semidefiniteness criterion at a local minimizer, localized to a neighborhood.

Let $d$ be a natural number, let $f : \mathrm{EuclideanSpace}(\mathbb{R}, \mathrm{Fin}\,d) \to \mathbb{R}$ , let $x_0$ be a point and $s$ a set with $s \in \mathcal{N}(x_0)$ . Suppose $f$ is twice continuously differentiable on $s$ and attains a local minimum at $x_0$ . Then for every direction $v$ ,

\langle D^2 f(x_0) v, v \rangle \ge 0.

Unlike the global version, this applies to functions that are only known to be regular near the minimizer, such as H"older functions arising as resolvent-graph components on a domain. It is the form needed at interior minimum points in maximum-principle arguments.

Formalization Note The quadratic form is expressed as (fderiv ℝ (fun y => fderiv ℝ f y v) x₀) v, and twice continuous differentiability on $s$ as ContDiffOn ℝ 2 f s.

Preamble

import Mathlib

open scoped Topology

Formal statement

namespace EthierKurtz

theorem hessian_posSemidef_of_isLocalMin_on {d : ℕ}
    {f : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ : EuclideanSpace ℝ (Fin d)}
    {s : Set (EuclideanSpace ℝ (Fin d))}
    (hs : ContDiffOn ℝ 2 f s) (hmem : s ∈ 𝓝 x₀)
    (hmin : IsLocalMin f x₀) (v : EuclideanSpace ℝ (Fin d)) :
    0 ≤ (fderiv ℝ (fun y => fderiv ℝ f y v) x₀) v := by sorry

end EthierKurtz

Source

Second partial derivative test, necessary direction, localized version. https://en.wikipedia.org/wiki/Second_partial_derivative_test

View graph