Nonnegative Directional Second Derivative at an Upper Touch

This technical lemma concerns a convex function $u:\mathbb R^n\to\mathbb R$ and a test function $\psi$. If $u$ is convex, $\psi\in C^2$ at $x_0$, $u(x_0)=\psi(x_0)$, and $u\le\psi$ almost everywhere in a neighborhood of $x_0$, then every direction $v\in\mathbb R^n$ satisfies

The result is a one-dimensional directional form of the positive-semidefinite Hessian conclusion used by the public touching lemma.

Original Lean declaration header

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

private lemma directional_second_deriv_nonneg
    {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)
    (v : EuclideanSpace ℝ (Fin n)) :
    0 ≤ bilinearIteratedFDerivTwo ℝ ψ x₀ v v

Module navigation

Module: Analysis/Convex/Viscosity.

Next: posSemidef_hessianMatrix_of_upper_touch.

Source excerpt, lines 26–32 · Frozen source 408915f.