Hessian operators and coordinate matrices

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

hessianOperator φ x is the continuous linear operator $D(\nabla\phi)(x):E\to E$ . For $\phi$ on EuclideanSpace ℝ (Fin n), Probability.Stein.hessianMatrix is the matrix whose $(i,j)$ entry is the bilinear second derivative $D^2\phi(y)[e_i,e_j]$ in the standard coordinate basis. These definitions provide operator and coordinate representations of the Hessian.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.Calculus
import FunctionalInequalities.Analysis.Operator.Coordinates
import FunctionalInequalities.Analysis.Cutoff.Profile
import Mathlib.LinearAlgebra.FiniteDimensional.Basic
import Mathlib.Analysis.InnerProductSpace.Adjoint

Original declaration excerpt

Shown in the original module context.

def hessianOperator (φ : E → ℝ) (x : E) : E →L[ℝ] E := fderiv ℝ (gradient φ) x

Module navigation

Direct project imports: Analysis/BakryEmery/Calculus, Analysis/Operator/Coordinates, Analysis/Cutoff/Profile.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.BakryEmery.HessianOperator · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Calculus
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Coordinates
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Cutoff_Profile
import Mathlib.LinearAlgebra.FiniteDimensional.Basic
import Mathlib.Analysis.InnerProductSpace.Adjoint

noncomputable section
open scoped ContDiff RealInnerProductSpace
open FunctionalInequalities.Analysis
namespace FunctionalInequalities
namespace Analysis
namespace BakryEmery
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
/-- The Hessian operator `∇²φ(x) = D(∇φ)(x) : E →L[ℝ] E`. The Euclidean coordinate object
`Probability.Stein.hessianMatrix` is its standard-basis entry matrix (`Probability.Stein.hessianMatrix_eq_operatorEntry_hessianOperator`). -/
def hessianOperator (φ : E → ℝ) (x : E) : E →L[ℝ] E := fderiv ℝ (gradient φ) x
end BakryEmery
end Analysis
end FunctionalInequalities
open FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Probability
namespace Stein
/-- The Hessian matrix `(∇²φ)_{ij}(y) = D²φ(y)(e_i, e_j)` of `φ` in the standard basis. -/
noncomputable def hessianMatrix {n : ℕ} (φ : EuclideanSpace ℝ (Fin n) → ℝ) (y : EuclideanSpace ℝ (Fin n)) : Probability.Stein.KernelMatrix n :=
  fun i j => bilinearIteratedFDerivTwo ℝ φ y (EuclideanSpace.basisFun (Fin n) ℝ i) (EuclideanSpace.basisFun (Fin n) ℝ j)
end Stein
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/HessianOperator.lean#L46-L557 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.HessianOperator`, definition bundle `KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator`; the repository is private at upload time).

View graph