Profile Inverse-Energy Drift Identity

Proved

FunctionalInequalities.Analysis.integral_profile_inverse_energy_eq_drift_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an identity for a compactly supported profile of a Monge–Ampère potential.

Let $u,V:\mathbb R^n\to\mathbb R$ satisfy the stated $C^1$ , Lipschitz-gradient, Lipschitz-exponent, and a.e. Monge–Ampère determinant hypotheses. Let $\zeta:\mathbb R\to\mathbb R$ be $C^1$ and assume $x\mapsto\zeta(u(x))$ has compact support. Then the weighted inverse-Hessian energy density

\zeta'(u) \sum_{i,j}(\nabla^2u)^{-1}_{ij}\,\partial_i u\,\partial_j u\,e^{-u}

is integrable, and

\int -\zeta'(u)\sum_{i,j}(\nabla^2u)^{-1}_{ij}\partial_i u\partial_j u\,e^{-u} =\int \zeta(u)\left(n-\nabla V(\nabla u)\cdot\nabla u\right)e^{-u}.

This result is a profile specialization of the weighted generator identity used in height-cutoff estimates.

Original Lean declaration header

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

private theorem integral_profile_inverse_energy_eq_drift {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {ζ : ℝ → ℝ} {G LF : NNReal}
    (hu : ContDiff ℝ 1 u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (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)))
    (hζ : ContDiff ℝ 1 ζ) (hζc : HasCompactSupport (fun x => ζ (u x))) :
    Integrable (fun x =>
      (deriv ζ (u x) * (∑ i : Fin n, ∑ j : Fin n, (hessianMatrix u x)⁻¹ i j *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j))) * Real.exp (-u x))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
    (∫ x, -(deriv ζ (u x) * (∑ i : Fin n, ∑ j : Fin n, (hessianMatrix u x)⁻¹ i j *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j))) * Real.exp (-u x)
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
    ∫ x, ζ (u x) * ((n : ℝ) - fderiv ℝ V (gradient u x) (gradient u x)) *
      Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

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

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

Supporting theorems: integrable_inv_hessianMatrix_mul_of_bounded_compact, integral_mul_generator_eq_neg_energy_of_contDiff_one.

Next: ae_hessianMatrix_comp_profile.

Source excerpt, lines 65–83 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_WeakCutoff

open MeasureTheory Filter Set Metric Matrix
open FunctionalInequalities.Probability.Stein

Formal statement

 theorem FunctionalInequalities.Analysis.integral_profile_inverse_energy_eq_drift_readable {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {ζ : ℝ → ℝ} {G LF : NNReal}
    (hu : ContDiff ℝ 1 u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (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)))
    (hζ : ContDiff ℝ 1 ζ) (hζc : HasCompactSupport (fun x => ζ (u x))) :
    Integrable (fun x =>
      (deriv ζ (u x) * (∑ i : Fin n, ∑ j : Fin n, (hessianMatrix u x)⁻¹ i j *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j))) * Real.exp (-u x))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
    (∫ x, -(deriv ζ (u x) * (∑ i : Fin n, ∑ j : Fin n, (hessianMatrix u x)⁻¹ i j *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j))) * Real.exp (-u x)
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
    ∫ x, ζ (u x) * ((n : ℝ) - fderiv ℝ V (gradient u x) (gradient u x)) *
      Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/InverseHessian/WeakCutoff.lean#L65-L137 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.InverseHessian.WeakCutoff`, declaration `_private.FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.InverseHessian.WeakCutoff.0.FunctionalInequalities.Analysis.integral_profile_inverse_energy_eq_drift`; the repository is private at upload time).

View graph