Two directional derivatives pass to a compactly supported convolution source

Proved

MeasureTheory.fderiv_convolution_right_apply_twice

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

convolutiondifferentiationmeasure-theory

Let K be a locally integrable real kernel on Euclidean n-space, and let f be a twice continuously differentiable real function with compact support. For any point x and any fixed vectors v,w, differentiation of the convolution twice passes to the source:

D_vD_w(K*f)(x)=(K*(D_vD_w f))(x).

The kernel need not be differentiable or integrable over the entire space. This generalizes the source-differentiation step in Hunter Eq. (2.26) from the Newtonian kernel and coordinate directions to any locally integrable kernel and arbitrary directions. Mathlib supplies the first Fréchet derivative of convolution; applying it twice gives this statement.

Preamble

import Mathlib.Analysis.Calculus.ContDiff.Convolution
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

open MeasureTheory ContinuousLinearMap
open scoped Convolution ContDiff

Formal statement

theorem MeasureTheory.fderiv_convolution_right_apply_twice (n : ℕ) (K f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hK : LocallyIntegrable K volume) (hf : ContDiff ℝ 2 f)
    (hfc : HasCompactSupport f) (x v w : EuclideanSpace ℝ (Fin n)) :
    fderiv ℝ (fun z => fderiv ℝ (K ⋆[lsmul ℝ ℝ] f) z w) x v =
      (K ⋆[lsmul ℝ ℝ] (fun y => fderiv ℝ (fun z => fderiv ℝ f z w) y v)) x := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch2.pdf, printed pp. 37–38, Theorem 2.26, Eqs. (2.26)–(2.28).

View graph