Weak Integration By Parts For The Closed Gradient

Proved

FunctionalInequalities.KLS.LogConcave.integral_mul_fderiv_eq_neg_integral_mul_inner_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem is the weak derivative identity for an element of the closed weighted-gradient domain.

Let $V$ be finite-dimensional, let $m$ be an additive Haar measure, let $\nu$ be log-concave with nonempty interior support, and let $U:V\to\mathbb R$ be continuous with $\nu=m.\operatorname{tilted}(-U)$ . Let

h\in D\!\left(\overline{T}_{\nu,m,I}\right),

where $I$ is the identity weight. For every $C^\infty$ compactly supported test function $\phi:V\to\mathbb R$ and every $w\in V$ ,

\int_V h(x)\,D\phi(x)[w] \,dm(x) = -\int_V \phi(x)\left\langle \overline{T}_{\nu,m,I}h(x),w\right\rangle\,dm(x).

The function $h$ is interpreted through its $L^2(\nu)$ representative, and the closed operator is closedWeightedOperator. This provides the weak gradient relation needed for identifying the kernel of the closed operator.

Original Lean declaration header

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

theorem integral_mul_fderiv_eq_neg_integral_mul_inner (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U)
    (h : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (w : V) :
    ∫ x, (h : Lp ℝ 2 (ν : Measure V)) x * fderiv ℝ φ x w ∂m =
      -∫ x, φ x * ⟪(hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi h :
        Lp V 2 (ν : Measure V)) x, w⟫ ∂m

Module navigation

Module: KLS/LogConcave/WeightedGradient/Kernel.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave.

Supporting theorems: exists_seq_smooth_tendsto_graph, tendsto_integral_mul_inner_of_tendsto, tendsto_integral_mul_of_tendsto.

Previous: tendsto_integral_mul_inner_of_tendsto · Next: integral_mul_fderiv_eq_zero_of_closedWeightedOperator_eq_zero.

Source excerpt, lines 339–346 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Kernel

open MeasureTheory Filter Topology InnerProductSpace
open scoped ContDiff RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] {U : V → ℝ}

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.integral_mul_fderiv_eq_neg_integral_mul_inner_readable (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U)
    (h : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (w : V) :
    ∫ x, (h : Lp ℝ 2 (ν : Measure V)) x * fderiv ℝ φ x w ∂m =
      -∫ x, φ x * ⟪(hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi h :
        Lp V 2 (ν : Measure V)) x, w⟫ ∂m := by sorry

Source

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

View graph