Zero Closed Gradient Implies Zero Weak Derivative Pairings

Proved

FunctionalInequalities.KLS.LogConcave.integral_mul_fderiv_eq_zero_of_closedWeightedOperator_eq_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem states the vanishing weak-gradient consequence of a zero closed weighted gradient.

Let $V$ , $m$ , $\nu$ , and $U$ satisfy the finite-dimensional, Haar, log-concavity, nonempty-support-interior, and tilted-law assumptions above. Let $h\in D(\overline{T}_{\nu,m,I})$ satisfy

\overline{T}_{\nu,m,I}h=0.

Then for every smooth compactly supported $\phi:V\to\mathbb R$ and every $w\in V$ ,

\int_V h(x)\,D\phi(x)[w] \,dm(x)=0.

This is an auxiliary kernel lemma: it converts the operator equation into vanishing distributional derivatives with respect to Haar measure. It does not itself identify $h$ as a constant.

Original Lean declaration header

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

theorem integral_mul_fderiv_eq_zero_of_closedWeightedOperator_eq_zero (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)
    (h0 : hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi h = 0) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (w : V) :
    ∫ x, (h : Lp ℝ 2 (ν : Measure V)) x * fderiv ℝ φ x w ∂m = 0

Module navigation

Module: KLS/LogConcave/WeightedGradient/Kernel.

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

Supporting theorems: integrable_exp_neg_of_eq_tilted, integral_mul_fderiv_eq_neg_integral_mul_inner.

Previous: integral_mul_fderiv_eq_neg_integral_mul_inner · Next: eq_const_mean_of_closedWeightedOperator_eq_zero.

Source excerpt, lines 424–430 · 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_zero_of_closedWeightedOperator_eq_zero_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)
    (h0 : hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi h = 0) {φ : V → ℝ}
    (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (w : V) :
    ∫ x, (h : Lp ℝ 2 (ν : Measure V)) x * fderiv ℝ φ x w ∂m = 0 := by sorry

Source

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

View graph