Compactly Supported Integration by Parts

Proved

FunctionalInequalities.Analysis.BakryEmery.integral_weightedLaplacian_mul_eq_neg_of_hasCompactSupport_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the compactly supported integration-by-parts identity for the weighted Laplacian.

Let $E$ be finite-dimensional, complete, and equipped with a real inner product; let $m$ be an additive Haar measure; and let $V,f,w:E\to\mathbb R$ . Assume that $V$ is $C^1$ , $f$ and $w$ are $C^2$ , and $w$ has compact support. Then

\int (\mathcal L_Vf)(x)w(x)\,d\bigl(m.\operatorname{tilted}(-V)\bigr)(x) =-\int\langle\nabla f(x),\nabla w(x)\rangle\,d\bigl(m.\operatorname{tilted}(-V)\bigr)(x).

Here weightedLaplacian V f is $\mathcal L_Vf$ . The result is the compact-support form of the first integration-by-parts equality.

Original Lean declaration header

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

theorem integral_weightedLaplacian_mul_eq_neg_of_hasCompactSupport {V f w : E → ℝ}
    (hV : ContDiff ℝ 1 V) (hf : ContDiff ℝ 2 f) (hw : ContDiff ℝ 2 w) (hwc : HasCompactSupport w) :
    ∫ x, weightedLaplacian V f x * w x ∂(m.tilted (-V)) =
      -∫ x, ⟪gradient f x, gradient w x⟫ ∂(m.tilted (-V))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/Temperate.

Definition modules: Analysis/BakryEmery/Laplacian.

Supporting theorems: cutoff_eq_one, hasCompactSupport_cutoff.

Next: integral_weightedLaplacian_mul_eq_neg_of_hasTemperateGrowth.

Source excerpt, lines 27–30 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_Temperate

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_hasCompactSupport_readable {V f w : E → ℝ}
    (hV : ContDiff ℝ 1 V) (hf : ContDiff ℝ 2 f) (hw : ContDiff ℝ 2 w) (hwc : HasCompactSupport w) :
    ∫ x, weightedLaplacian V f x * w x ∂(m.tilted (-V)) =
      -∫ x, ⟪gradient f x, gradient w x⟫ ∂(m.tilted (-V)) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/Temperate.lean#L25-L117 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.Temperate`, declaration `FunctionalInequalities.Analysis.BakryEmery.integral_weightedLaplacian_mul_eq_neg_of_hasCompactSupport`; the repository is private at upload time).

View graph