Compact Diffusion Pairing Identity

Proved

FunctionalInequalities.KLS.LogConcave.compact_pairing_identity_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem gives the integration-by-parts identity for a compactly supported diffusion test.

Let $E$ be finite-dimensional with its real inner-product structure, let $m$ be an additive Haar measure, let $\nu$ be a probability measure, and let $U:E\to\mathbb R$ satisfy $\nu=m.\operatorname{tilted}(-U)$ . Assume $U$ and $f$ are $C^1$ , while $u:E\to\mathbb R$ is $C^\infty$ and compactly supported. Then both functions

f(x)\,[-\mathcal L_Uu(x)] \quad\text{and}\quad \langle\nabla f(x),\nabla u(x)\rangle

are integrable with respect to $\nu$ , and

\int_E f(x)\,[-\mathcal L_Uu(x)]\,d\nu(x) = \int_E \langle\nabla f(x),\nabla u(x)\rangle\,d\nu(x),

where weightedLaplacian denotes $\mathcal L_U$ . The function $f$ need not be compactly supported.

Original Lean declaration header

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

theorem compact_pairing_identity
    {ν : ProbabilityMeasure E} (m : Measure E) [m.IsAddHaarMeasure]
    {U f u : E → ℝ} (hνU : (ν : Measure E) = m.tilted (-U))
    (hU : ContDiff ℝ 1 U) (hf : ContDiff ℝ 1 f)
    (hu : ContDiff ℝ ∞ u) (huc : HasCompactSupport u) :
    Integrable (fun x => f x * (-weightedLaplacian U u x)) (ν : Measure E) ∧
      Integrable (fun x => ⟪gradient f x, gradient u x⟫) (ν : Measure E) ∧
      (∫ x, f x * (-weightedLaplacian U u x) ∂(ν : Measure E)) =
        ∫ x, ⟪gradient f x, gradient u x⟫ ∂(ν : Measure E)

Module navigation

Module: KLS/LogConcave/BrascampLieb.

Definition modules: Analysis/BakryEmery/Laplacian.

Previous: inner_center_left_of_mean_zero.

Source excerpt, lines 105–113 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BrascampLieb

open MeasureTheory Filter Topology Set InnerProductSpace
open FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.compact_pairing_identity_readable
    {ν : ProbabilityMeasure E} (m : Measure E) [m.IsAddHaarMeasure]
    {U f u : E → ℝ} (hνU : (ν : Measure E) = m.tilted (-U))
    (hU : ContDiff ℝ 1 U) (hf : ContDiff ℝ 1 f)
    (hu : ContDiff ℝ ∞ u) (huc : HasCompactSupport u) :
    Integrable (fun x => f x * (-weightedLaplacian U u x)) (ν : Measure E) ∧
      Integrable (fun x => ⟪gradient f x, gradient u x⟫) (ν : Measure E) ∧
      (∫ x, f x * (-weightedLaplacian U u x) ∂(ν : Measure E)) =
        ∫ x, ⟪gradient f x, gradient u x⟫ ∂(ν : Measure E) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/BrascampLieb.lean#L103-L143 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.BrascampLieb`, declaration `FunctionalInequalities.KLS.LogConcave.compact_pairing_identity`; the repository is private at upload time).

View graph