Multi-index differentiation of convolution with a test function

Proved

HunterPDE.Sobolev.iteratedPartial_convolution_testFunction

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

convolutiondifferentiationweak-derivatives

Let u be a smooth compactly supported scalar function on Euclidean n-space and let f be locally integrable. For every multi-index alpha, the classical ordered multi-index derivative of u*f equals (D^alpha u)*f, as an equality of functions. No global integrability, positivity or normalization is assumed. The proof iterates compact-kernel differentiation under the integral, with compact support and smoothness preserved at every step. All derivative orders and dimension zero are included.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Mathlib.Analysis.Calculus.ContDiff.Convolution
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.Tactic.Ring

open MeasureTheory ContinuousLinearMap HunterPDE.Sobolev
open scoped Convolution ContDiff
set_option autoImplicit false

Formal statement

theorem HunterPDE.Sobolev.iteratedPartial_convolution_testFunction {n : ℕ} (α : Fin n → ℕ)
    {u f : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : IsTestFunction Set.univ u) (hf : LocallyIntegrable f) :
    iteratedPartial α (u ⋆[lsmul ℝ ℝ, volume] f) =
      (iteratedPartial α u ⋆[lsmul ℝ ℝ, volume] f) := by sorry

Source

John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, Theorem 3.19 proof (printed p. 55), using Theorem 1.28 (printed pp. 12–13). Derived multi-index calculus interfaces for arbitrary smooth compact kernels; the reflection rule follows the ordinary chain rule.

View graph