Convexity from a Nonnegative Hessian Lower Bound

Proved

FunctionalInequalities.Analysis.BakryEmery.convexOn_of_hessian_ge_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the standard convexity implication from a pointwise Hessian lower bound.

Let $E$ be a real inner-product space and let $U:E\to\mathbb R$ be $C^2$ . Let $\rho\geq0$ and suppose that for every $x,v\in E$ ,

\rho\,\|v\|^2\leq D^2U(x)(v,v).

Then $U$ is convex on all of $E$ :

U\text{ is convex on }E.

The Hessian is represented by bilinearIteratedFDerivTwo, and no completeness or finite-dimensionality assumption is required. The result may be used to convert curvature-type Hessian hypotheses into global convexity.

Original Lean declaration header

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

theorem convexOn_of_hessian_ge {U : E → ℝ} (hU : ContDiff ℝ 2 U) {ρ : ℝ} (hρ : 0 ≤ ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v) :
    ConvexOn ℝ Set.univ U

Module navigation

Module: Analysis/BakryEmery/Curvature.

Next: integrable_weightedLaplacian_gamma.

Source excerpt, lines 39–41 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Curvature

universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E]
omit [CompleteSpace E] [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.convexOn_of_hessian_ge_readable {U : E → ℝ} (hU : ContDiff ℝ 2 U) {ρ : ℝ} (hρ : 0 ≤ ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v) :
    ConvexOn ℝ Set.univ U := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Curvature.lean#L37-L99 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Curvature`, declaration `FunctionalInequalities.Analysis.BakryEmery.convexOn_of_hessian_ge`; the repository is private at upload time).

View graph