Semidefinite Hessian at an Upper Touch

Let $u,\psi:\mathbb R^n\to\mathbb R$, with $u$ convex. If $\psi\in C^2$ at $x_0$, $u(x_0)=\psi(x_0)$, and $u(x)\le\psi(x)$ in a neighborhood of $x_0$, then the coordinate Hessian of $\psi$ at $x_0$ is positive semidefinite:

This is a pointwise viscosity touching principle for convex functions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem posSemidef_hessianMatrix_of_upper_touch {n : ℕ} {u ψ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) {x₀ : EuclideanSpace ℝ (Fin n)} (hψ : ContDiffAt ℝ 2 ψ x₀)
    (hcontact : u x₀ = ψ x₀) (htouch : ∀ᶠ x in 𝓝 x₀, u x ≤ ψ x) :
    (hessianMatrix ψ x₀).PosSemidef

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: directional_second_deriv_nonneg.

Previous: directional_second_deriv_nonneg · Next: hessianMatrix_quadratic.

Source excerpt, lines 149–152 · Frozen source 408915f.