Mollification Commutes with Weak Directional Differentiation

This is the generic weak-derivative identity for mollification.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $f,g:E\to\mathbb{R}$ and $v\in E$, and assume HasWeakDerivAlong f g v. Let $\varphi$ be a smooth compactly supported bump centered at $0$, and let $x\in E$. Then

In Lean, the directional derivative is fderiv ℝ (...) x v, and the convolution uses volume measure. This identifies the classical derivative of the mollified function with the mollification of the weak derivative.

Original Lean declaration header

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

theorem fderiv_convolution_eq_of_hasWeakDerivAlong {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {f g : E → ℝ} {v : E} (h : HasWeakDerivAlong f g v) (φ : ContDiffBump (0 : E)) (x : E) :
    fderiv ℝ (convolution (φ.normed volume) f (ContinuousLinearMap.lsmul ℝ ℝ) volume) x v =
      convolution (φ.normed volume) g (ContinuousLinearMap.lsmul ℝ ℝ) volume x

Module navigation

Module: Analysis/WeakDerivative/Mollification.

Definition modules: Analysis/WeakDerivative/Basic.

Next: quotient_pairing_tendsto.

Source excerpt, lines 25–29 · Frozen source 408915f.