Integrability of Compactly Supported Gradients Under Tilting

Proved

FunctionalInequalities.Analysis.BakryEmery.integrable_gradient_expTilt_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem establishes integrability of the gradient of a compactly supported function under every exponential tilt.

Let $E$ be a finite-dimensional complete real inner-product space, let $m$ be a measure on $E$ , and let $V,f:E\to\mathbb R$ . If $f$ is $C^2$ and has compact support, then for every $z\in E$ ,

\nabla f\in L^1\!\left(\operatorname{expTilt}\bigl(m.\operatorname{tilted}(-V),z\bigr)\right).

No regularity or integrability hypothesis on $V$ is present in the type. This is a technical ingredient for integration by parts and tilt-average identities.

Original Lean declaration header

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

theorem integrable_gradient_expTilt {V f : E → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f)
    (z : E) : Integrable (gradient f) (expTilt (m.tilted (-V)) z)

Module navigation

Module: Analysis/BakryEmery/Tilt/Basic.

Previous: expTilt_tilted · Next: tiltAverage_neg_weightedLaplacian.

Source excerpt, lines 122–123 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Basic

open MeasureTheory FunctionalInequalities.Analysis.Tensor
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable (m : MeasureTheory.Measure E) [m.IsAddHaarMeasure]
omit [m.IsAddHaarMeasure]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.integrable_gradient_expTilt_readable {V f : E → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f)
    (z : E) : Integrable (gradient f) (expTilt (m.tilted (-V)) z) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Basic.lean#L119-L137 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.integrable_gradient_expTilt`; the repository is private at upload time).

View graph