Integrability of Shifted Hessian Increment Energy

Proved

FunctionalInequalities.Analysis.integrable_hessian_increment_energy_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is an integrability component related to Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $u$ be continuous with Lipschitz gradient, let $\eta$ be continuous and compactly supported, and let $h$ be any vector in $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))$ . Then the function

x\mapsto \eta(x)\left(\sum_{i,j}\bigl(H(x+h)_{ij}-H(x)_{ij}\bigr)^2+\sum_{i,j}\bigl(H(x-h)_{ij}-H(x)_{ij}\bigr)^2\right)e^{-u(x)},

where $H(x)=\operatorname{hessianMatrix}(u,x)$ , is integrable with respect to volume.

This statement provides genuine $L^1$ control for the compactly weighted squared Hessian increments. It does not assert the main integrated Hessian bound.

Original Lean declaration header

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

theorem integrable_hessian_increment_energy {n : ℕ}
    {u η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : Continuous u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hη : Continuous η) (hηc : HasCompactSupport η)
    (h : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun x => η x *
      ((∑ i, ∑ j, (hessianMatrix u (x + h) - hessianMatrix u x) i j ^ 2) +
       ∑ i, ∑ j, (hessianMatrix u (x - h) - hessianMatrix u x) i j ^ 2) *
      Real.exp (-u x)) (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/Convex/HessianIncrement.

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

Supporting theorems: norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Next: integral_mul_hessian_increment_le.

Source excerpt, lines 36–44 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_HessianIncrement

open MeasureTheory Set Filter
open FunctionalInequalities.Probability.Stein

Formal statement


theorem FunctionalInequalities.Analysis.integrable_hessian_increment_energy_readable {n : ℕ}
    {u η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : Continuous u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hη : Continuous η) (hηc : HasCompactSupport η)
    (h : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun x => η x *
      ((∑ i, ∑ j, (hessianMatrix u (x + h) - hessianMatrix u x) i j ^ 2) +
       ∑ i, ∑ j, (hessianMatrix u (x - h) - hessianMatrix u x) i j ^ 2) *
      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/Convex/HessianIncrement.lean#L34-L108 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.HessianIncrement`, declaration `FunctionalInequalities.Analysis.integrable_hessian_increment_energy`; the repository is private at upload time).

View graph