Coordinate densities for weak inverse-Hessian identities

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For functions on EuclideanSpace ℝ (Fin n), coord f i x is the directional derivative $Df(x)[e_i]$ , weightedTest u a f i x is $a(x)e^{-u(x)}\,\operatorname{coord}(f,i,x)$ , and energyDensity u a f x is $e^{-u(x)}$ times the inverse-Hessian contraction $\sum_{i,j}(\nabla^2u(x))^{-1}_{ij}\,\operatorname{coord}(a,i,x)\operatorname{coord}(f,j,x)$ . generatorDensity u V a f x is $a(x)e^{-u(x)}$ times $\operatorname{tr}((\nabla^2u(x))^{-1}\nabla^2f(x))-DV(\nabla u(x))[\nabla f(x)]$ . These private definitions support the weak integration-by-parts identities; the displayed bundle does not change their stated measurability or regularity assumptions.

Original module imports

import FunctionalInequalities.Analysis.Matrix.WeakDerivative
import FunctionalInequalities.Analysis.Matrix.Piola
import FunctionalInequalities.Analysis.Cutoff.LipschitzBall
import FunctionalInequalities.Analysis.WeakDerivative.Basic
import FunctionalInequalities.Analysis.WeakDerivative.Calculus
import FunctionalInequalities.Analysis.BakryEmery.HessianOperator
import FunctionalInequalities.Analysis.BakryEmery.WeakHessian
import Mathlib.Analysis.Calculus.Rademacher
import Mathlib.LinearAlgebra.Matrix.Hermitian
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Trace
import Mathlib.Data.Real.Star

Original declaration excerpt

Shown in the original module context.

private abbrev coord {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (i : Fin n) (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  fderiv ℝ f x (EuclideanSpace.basisFun (Fin n) ℝ i)

Module navigation

Direct project imports: Analysis/Matrix/WeakDerivative, Analysis/Matrix/Piola, Analysis/Cutoff/LipschitzBall, Analysis/WeakDerivative/Basic, Analysis/WeakDerivative/Calculus, Analysis/BakryEmery/HessianOperator, Analysis/BakryEmery/WeakHessian.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.InverseHessian.Weak · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_WeakDerivative
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Piola
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Cutoff_LipschitzBall
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Calculus
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_WeakHessian
import Mathlib.Analysis.Calculus.Rademacher
import Mathlib.LinearAlgebra.Matrix.Hermitian
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Trace
import Mathlib.Data.Real.Star

noncomputable section
section GeneratorIdentities
open MeasureTheory Set Filter
open scoped Topology RealInnerProductSpace
open FunctionalInequalities.Probability.Stein
namespace FunctionalInequalities
namespace Analysis
 abbrev coord {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (i : Fin n) (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  fderiv ℝ f x (EuclideanSpace.basisFun (Fin n) ℝ i)
 def weightedTest {n : ℕ}
    (u a f : EuclideanSpace ℝ (Fin n) → ℝ) (i : Fin n)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  a x * Real.exp (-u x) * FunctionalInequalities.Analysis.coord f i x
 def energyDensity {n : ℕ}
    (u a f : EuclideanSpace ℝ (Fin n) → ℝ)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  (∑ i, ∑ j, (hessianMatrix u x)⁻¹ i j * FunctionalInequalities.Analysis.coord a i x * FunctionalInequalities.Analysis.coord f j x) *
    Real.exp (-u x)
 def generatorDensity {n : ℕ}
    (u V a f : EuclideanSpace ℝ (Fin n) → ℝ)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  a x * (((hessianMatrix u x)⁻¹ * hessianMatrix f x).trace -
    fderiv ℝ V (gradient u x) (gradient f x)) * Real.exp (-u x)
end Analysis
end FunctionalInequalities
end GeneratorIdentities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.lean#L383-L402 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.InverseHessian.Weak`, definition bundle `KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak`; the repository is private at upload time).

View graph