Prove2Me

Gradient of a Mollified Scalar Function

Proved
FunctionalInequalities.Analysis.gradient_convolution_normed_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma identifies the gradient of a mollified scalar function.

Let EE be a finite-dimensional real inner-product space with its Borel structure. Let U:E→RU:E\to\mathbb R be C1C^1 and suppose that ∇U\nabla U is Lipschitz with constant G∈[0,∞)G\in[0,\infty). For every smooth compactly supported bump φ\varphi,

∇(φnorm ⁣∗U)=φnorm ⁣∗∇U.\nabla\bigl(\varphi^{\mathrm{norm}}\!\ast U\bigr) = \varphi^{\mathrm{norm}}\!\ast\nabla U.

The convolution is with respect to volume measure and scalar multiplication is represented by ContinuousLinearMap.lsmul. This technical identity supports approximation by smooth convolutions.

Original Lean declaration header

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

private lemma gradient_convolution_normed
    {U : E → ℝ} (hU : ContDiff ℝ 1 U)
    {G : NNReal} (hG : LipschitzWith G (gradient U))
    (φ : ContDiffBump (0 : E)) :
    gradient
        (convolution
          (φ.normed (volume : Measure E)) U
          (ContinuousLinearMap.lsmul ℝ ℝ) (volume : Measure E)) =
      convolution
        (φ.normed (volume : Measure E)) (gradient U)
        (ContinuousLinearMap.lsmul ℝ ℝ) (volume : Measure E)

Module navigation

Module: Analysis/Mollification/Hessian.

Next: exists_contDiff_approx_of_lipschitz_gradient.

Source excerpt, lines 85–95 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Hessian

open MeasureTheory Filter
variable {E : Type*}
variable [NormedAddCommGroup E]
variable [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
Formal statement
 lemma FunctionalInequalities.Analysis.gradient_convolution_normed_readable
    {U : E → ℝ} (hU : ContDiff ℝ 1 U)
    {G : NNReal} (hG : LipschitzWith G (gradient U))
    (φ : ContDiffBump (0 : E)) :
    gradient
        (convolution
          (φ.normed (volume : Measure E)) U
          (ContinuousLinearMap.lsmul ℝ ℝ) (volume : Measure E)) =
      convolution
        (φ.normed (volume : Measure E)) (gradient U)
        (ContinuousLinearMap.lsmul ℝ ℝ) (volume : Measure E) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Mollification/Hessian.lean#L85-L266 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Mollification.Hessian`, declaration `_private.FunctionalInequalities.Analysis.Mollification.Hessian.0.FunctionalInequalities.Analysis.gradient_convolution_normed`; the repository is private at upload time).

View graph