Hessian matrix in an orthonormal basis

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_MongeAmpere

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a finite-dimensional real inner-product space $E$ , a function $\varphi : E \to \mathbb{R}$ , an orthonormal basis $b$ indexed by Fin m, and $x \in E$ , hessianMatrixIn φ b x is the matrix with entries $D^2\varphi(x)(b_i,b_j)$ . The module also contains supporting infrastructure for the Monge–Ampère log-determinant identities and positivity statements described in its header, but the listed declaration is this Hessian-coordinate definition.

Original module imports

import FunctionalInequalities.Analysis.Operator.Coordinates
import FunctionalInequalities.Analysis.BakryEmery.HessianOperator
import FunctionalInequalities.Analysis.Matrix.DeterminantDerivative
import FunctionalInequalities.Analysis.Matrix.Positivity
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.Analysis.Matrix.Normed
import Mathlib.Analysis.Normed.Module.FiniteDimension

Original declaration excerpt

Shown in the original module context.

def hessianMatrixIn {m : ℕ} (φ : E → ℝ) (b : OrthonormalBasis (Fin m) ℝ E) (x : E) :
    Matrix (Fin m) (Fin m) ℝ :=
  fun i j => bilinearIteratedFDerivTwo ℝ φ x (b i) (b j)

Module navigation

Direct project imports: Analysis/Operator/Coordinates, Analysis/BakryEmery/HessianOperator, Analysis/Matrix/DeterminantDerivative, Analysis/Matrix/Positivity.

Theorems in source order:

hessianMatrixIn_posSemidef

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Coordinates
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_DeterminantDerivative
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.Analysis.Matrix.Normed
import Mathlib.Analysis.Normed.Module.FiniteDimension

noncomputable section
open scoped ContDiff RealInnerProductSpace Matrix.Norms.Elementwise
open FunctionalInequalities.Analysis
open Filter Topology
namespace FunctionalInequalities
namespace Analysis
namespace BakryEmery
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
/-- The Hessian matrix `(D²φ(x)(b i, b j))_{ij}` of `φ` in an orthonormal basis `b`. -/
def hessianMatrixIn {m : ℕ} (φ : E → ℝ) (b : OrthonormalBasis (Fin m) ℝ E) (x : E) :
    Matrix (Fin m) (Fin m) ℝ :=
  fun i j => bilinearIteratedFDerivTwo ℝ φ x (b i) (b j)
end BakryEmery
end Analysis
end FunctionalInequalities

Source

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

View graph