Derivative of a Mollified Lipschitz Map

This establishes the derivative formula for convolution with a normalized smooth bump.

Let $E$ be a finite-dimensional real inner-product space with its Borel structure. Let $F:E\to E$ be Lipschitz with Lipschitz bound $G\in[0,\infty)$, let $\varphi$ be a smooth compactly supported bump centered at $0$, and let $x\in E$. Then the convolution of $F$ with the normalized bump $\varphi^{\mathrm{norm}}$ has a Fréchet derivative at $x$ given by the convolution of the almost-everywhere derivative of $F$:

In Lean, the convolution uses ContinuousLinearMap.lsmul, volume measure, and fderiv ℝ F. This is a supporting result for mollification identities.

Original Lean declaration header

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

theorem hasFDerivAt_convolution_normed_of_lipschitz
    {F : E → E} {G : NNReal} (hF : LipschitzWith G F) (φ : ContDiffBump (0 : E)) (x : E) :
    HasFDerivAt (φ.normed (volume : Measure E) ⋆[ContinuousLinearMap.lsmul ℝ ℝ, (volume : Measure E)] F)
      ((φ.normed (volume : Measure E) ⋆[ContinuousLinearMap.lsmul ℝ ℝ, (volume : Measure E)]
        fderiv ℝ F) x) x

Module navigation

Module: Analysis/Mollification/Basic.

Supporting theorems: integral_fderiv_kernel_eq.

Previous: integral_fderiv_kernel_eq.

Source excerpt, lines 516–520 · Frozen source 408915f.