Gradient Commutation with Mollification

Proved

FunctionalInequalities.Analysis.Mollification.gradient_convolution_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This states that mollification commutes with the gradient for smooth compactly supported scalar functions.

Let $V$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure, and let $\varphi$ be a smooth bump centered at $0$ . If $g:V\to\mathbb{R}$ is smooth and compactly supported, then for every $x\in V$ ,

\nabla\bigl((\varphi_{\mathrm{normed}}\ast g)(x)\bigr) =\bigl(\varphi_{\mathrm{normed}}\ast\nabla g\bigr)(x).

The gradient on the right is vector-valued, and the convolution uses the scalar multiplication continuous linear map. This identity is useful for transferring differential estimates through mollification.

Original Lean declaration header

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

theorem gradient_convolution {g : V → ℝ} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g)
    (x : V) :
    gradient (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] g) x =
      (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] gradient g) x

Module navigation

Module: Analysis/Mollification/Basic.

Previous: integral_inner_convolution_eq · Next: laplacian_convolution.

Source excerpt, lines 360–363 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic

open scoped Convolution ContDiff ENNReal RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {m : MeasureTheory.Measure V} [m.IsAddHaarMeasure]
variable (φ : ContDiffBump (0 : V))

Formal statement


theorem FunctionalInequalities.Analysis.Mollification.gradient_convolution_readable {g : V → ℝ} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g)
    (x : V) :
    gradient (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] g) x =
      (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] gradient g) x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Mollification/Basic.lean#L358-L385 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Mollification.Basic`, declaration `FunctionalInequalities.Analysis.Mollification.gradient_convolution`; the repository is private at upload time).

View graph