Weighted Weak Inverse-Hessian Generator Identity

Proved

FunctionalInequalities.Analysis.integral_mul_generator_eq_neg_energy_of_contDiff_one_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is a weak inverse-Hessian integration-by-parts identity associated with equation (2.2) of Letwin (arXiv:2607.24164v1), and supports Lemma A.4.

Let $u,V,w,\eta:\mathbb R^n\to\mathbb R$ be $C^1$ , with $u$ having Lipschitz gradient, $V$ having the stated $C^1$ regularity, and $w$ having Lipschitz gradient. Assume $-u+V\circ\nabla u$ is Lipschitz and

\det\nabla^2u=\exp(-u+V(\nabla u))

a.e. Assume that $\eta$ is compactly supported. Then

\int \eta(x)\left(\operatorname{tr}\bigl((\nabla^2u(x))^{-1}\nabla^2w(x)\bigr) -\nabla V(\nabla u(x))\cdot\nabla w(x)\right)e^{-u(x)}\,dx

=-\int\left(\sum_{i,j}(\nabla^2u(x))^{-1}_{ij}\,\partial_i\eta(x)\,\partial_jw(x)\right)e^{-u(x)}\,dx.

The statement uses only $C^1$ regularity for the displayed functions and supplies the weighted generator–energy identity for compact multipliers.

Original Lean declaration header

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

theorem integral_mul_generator_eq_neg_energy_of_contDiff_one {n : ℕ} {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hw : ContDiff ℝ 1 w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 1 η) (hηc : HasCompactSupport η) :
    ∫ x, η x * (((hessianMatrix u x)⁻¹ * hessianMatrix w x).trace -
        fderiv ℝ V (gradient u x) (gradient w x)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      -∫ x, (∑ i, ∑ j, (hessianMatrix u x)⁻¹ i j *
          fderiv ℝ η x (EuclideanSpace.basisFun (Fin n) ℝ i) *
          fderiv ℝ w x (EuclideanSpace.basisFun (Fin n) ℝ j)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates.

Supporting theorems: integrable_inv_hessianMatrix_mul_of_bounded_compact, exists_lipschitzWith_smul_of_locallyLipschitz, assemble_generator.

Previous: hasWeakDerivAlong_inverse_hessian_of_logdet · Next: ae_inverse_hessian_row_divergence_of_weak_derivative.

Source excerpt, lines 1152–1165 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak

open MeasureTheory
open FunctionalInequalities.Probability.Stein

Formal statement


theorem FunctionalInequalities.Analysis.integral_mul_generator_eq_neg_energy_of_contDiff_one_readable {n : ℕ} {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hw : ContDiff ℝ 1 w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 1 η) (hηc : HasCompactSupport η) :
    ∫ x, η x * (((hessianMatrix u x)⁻¹ * hessianMatrix w x).trace -
        fderiv ℝ V (gradient u x) (gradient w x)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      -∫ x, (∑ i, ∑ j, (hessianMatrix u x)⁻¹ i j *
          fderiv ℝ η x (EuclideanSpace.basisFun (Fin n) ℝ i) *
          fderiv ℝ w x (EuclideanSpace.basisFun (Fin n) ℝ j)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.lean#L1150-L1177 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.InverseHessian.Weak`, declaration `FunctionalInequalities.Analysis.integral_mul_generator_eq_neg_energy_of_contDiff_one`; the repository is private at upload time).

View graph