Vanishing Integral Difference Under a Zero Weak Gradient

Proved

FunctionalInequalities.Energy.Euclidean.integral_mul_sub_translate_eq_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This derives a translation identity from a zero weak gradient.

Let $V$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $m$ be a measure on $V$ , and let $h:V\to\mathbb R$ be locally integrable. Assume that for every smooth compactly supported test function $\psi$ and every direction $w\in V$ ,

\int h(x)D\psi(x)w\,dm(x)=0.

Then, for every smooth compactly supported $\phi$ and every $v\in V$ ,

\int h(x)\bigl(\phi(x)-\phi(x-v)\bigr)\,dm(x)=0.

The statement is an intermediate translation-invariance identity in the argument that a locally integrable function with zero weak gradient is almost everywhere constant.

Formalization Note The quantification over test functions includes the stated smoothness and compact-support hypotheses, and no Haar-measure assumption is required here.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.Euclidean. Shown in its original module context. Proof omitted.

theorem integral_mul_sub_translate_eq_zero {h : V → ℝ} (hh : LocallyIntegrable h m)
    (h0 : ∀ φ : V → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → ∀ w : V,
      ∫ x, h x * fderiv ℝ φ x w ∂m = 0)
    {φ : V → ℝ} (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (v : V) :
    ∫ x, h x * (φ x - φ (x - v)) ∂m = 0

Module navigation

Module: Energy/Euclidean/ZeroGradient.

Supporting theorems: hasDerivAt_integral_mul_translate.

Previous: hasDerivAt_integral_mul_translate · Next: locallyIntegrable_comp_add_right.

Source excerpt, lines 165–169 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_ZeroGradient

open MeasureTheory Filter Topology
open scoped ContDiff
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure]
omit [m.IsAddHaarMeasure]

Formal statement


theorem FunctionalInequalities.Energy.Euclidean.integral_mul_sub_translate_eq_zero_readable {h : V → ℝ} (hh : LocallyIntegrable h m)
    (h0 : ∀ φ : V → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → ∀ w : V,
      ∫ x, h x * fderiv ℝ φ x w ∂m = 0)
    {φ : V → ℝ} (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) (v : V) :
    ∫ x, h x * (φ x - φ (x - v)) ∂m = 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/ZeroGradient.lean#L163-L248 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.ZeroGradient`, declaration `FunctionalInequalities.Energy.Euclidean.integral_mul_sub_translate_eq_zero`; the repository is private at upload time).

View graph