Integration by Parts for Temperate-Growth Functions

Proved

FunctionalInequalities.Analysis.BakryEmery.integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $E$ be finite-dimensional and complete with a real inner product, let $m$ be an additive Haar measure, and let $V,f,g:E\to\mathbb R$ . Assume:

$V$ is $C^1$ .
$\|\nabla V(x)\|\le C_V(1+\|x\|)^{k_V}$ for some $C_V\in\mathbb R$ and $k_V\in\mathbb N$ .
Every exponential moment is integrable for $m.\operatorname{tilted}(-V)$ .
$f$ and $g$ have HasTemperateGrowth.

Then

\int (\mathcal L_Vf)g\,d\mu=-\int\langle\nabla f,\nabla g\rangle\,d\mu, \qquad \mu=m.\operatorname{tilted}(-V).

This is the first equality in the temperate-growth integration-by-parts formula and is reusable for weighted diffusion identities.

Original Lean declaration header

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

theorem integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth {V f g : E → ℝ}
    (hV : ContDiff ℝ 1 V) {CV : ℝ} {kV : ℕ} (hVg : ∀ x, ‖gradient V x‖ ≤ CV * (1 + ‖x‖) ^ kV)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : f.HasTemperateGrowth) (hg : g.HasTemperateGrowth) :
    ∫ x, weightedLaplacian V f x * g x ∂(m.tilted (-V)) =
      -∫ x, ⟪gradient f x, gradient g x⟫ ∂(m.tilted (-V))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/Temperate.

Definition modules: Analysis/BakryEmery/Laplacian.

Selected supporting theorems: abs_laplacian_le, cutoff_eq_one, hasCompactSupport_cutoff, integrable_of_norm_le_pow, integral_weightedLaplacian_mul_eq_neg_of_hasCompactSupport.

Previous: integral_weightedLaplacian_mul_eq_neg_of_hasCompactSupport.

Source excerpt, lines 162–167 · Frozen source 408915f.

Literature

This formalizes Equation (15) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited as Equation (15), p. 6.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_Temperate

open MeasureTheory Filter Topology
open scoped RealInnerProductSpace ContDiff
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]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth_readable {V f g : E → ℝ}
    (hV : ContDiff ℝ 1 V) {CV : ℝ} {kV : ℕ} (hVg : ∀ x, ‖gradient V x‖ ≤ CV * (1 + ‖x‖) ^ kV)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : f.HasTemperateGrowth) (hg : g.HasTemperateGrowth) :
    ∫ x, weightedLaplacian V f x * g x ∂(m.tilted (-V)) =
      -∫ x, ⟪gradient f x, gradient g x⟫ ∂(m.tilted (-V)) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Equation (15), p. 6 (unnumbered). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/Temperate.lean#L161-L287 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.Temperate`, declaration `FunctionalInequalities.Analysis.BakryEmery.integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth`; the repository is private at upload time).

View graph