Prove2Me

Derivative Kernel Integration Identity

Proved
FunctionalInequalities.Analysis.integral_fderiv_kernel_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This technical lemma gives an integration-by-parts identity for a Lipschitz change of variables.

Let EE be a finite-dimensional real inner-product space equipped with its Borel measure. Let F:E→EF:E\to E be Lipschitz with constant bounded by G∈[0,∞)G\in[0,\infty), let k:E→Rk:E\to\mathbb R be C1C^1 with compact support, let x,v∈Ex,v\in E, and let ℓ:E→R\ell:E\to\mathbb R be continuous linear. Then

∫Dk(t)[v] ℓ(F(x−t)) dt=∫k(t) ℓ ⁣(DF(x−t)[v]) dt.\int \mathrm Dk(t)[v]\,\ell(F(x-t))\,dt = \int k(t)\,\ell\!\left(DF(x-t)[v]\right)\,dt.

The derivative DFDF is fderiv ℝ F and is used pointwise in the displayed expression. The result is used to establish derivative formulas for mollified Lipschitz maps.

Original Lean declaration header

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

private theorem integral_fderiv_kernel_eq
    {F : E → E} {G : NNReal} (hF : LipschitzWith G F)
    (k : E → ℝ) (hk : ContDiff ℝ 1 k) (hc : HasCompactSupport k)
    (x v : E) (ℓ : E →L[ℝ] ℝ) :
    (∫ t, fderiv ℝ k t v * ℓ (F (x - t))) =
      ∫ t, k t * ℓ (fderiv ℝ F (x - t) v)

Module navigation

Module: Analysis/Mollification/Basic.

Previous: laplacian_convolution · Next: hasFDerivAt_convolution_normed_of_lipschitz.

Source excerpt, lines 456–461 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic

variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
variable [BorelSpace E]
Formal statement
 theorem FunctionalInequalities.Analysis.integral_fderiv_kernel_eq_readable
    {F : E → E} {G : NNReal} (hF : LipschitzWith G F)
    (k : E → ℝ) (hk : ContDiff ℝ 1 k) (hc : HasCompactSupport k)
    (x v : E) (ℓ : E →L[ℝ] ℝ) :
    (∫ t, fderiv ℝ k t v * ℓ (F (x - t))) =
      ∫ t, k t * ℓ (fderiv ℝ F (x - t) v) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Mollification/Basic.lean#L456-L510 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Mollification.Basic`, declaration `_private.FunctionalInequalities.Analysis.Mollification.Basic.0.FunctionalInequalities.Analysis.integral_fderiv_kernel_eq`; the repository is private at upload time).

View graph