Prove2Me

Directional derivatives commute with mollification of C1C^1 functions on C\mathbb{C}

Proved
JHolomorphic.fderiv_normed_convolution_apply

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

convolutionmollifiersweak-derivatives

Let φ:C→R\varphi:\mathbb{C}\to\mathbb{R} be C1C^1 with compact support, let ρ\rho be a bump function centred at 00 and let ρn=ρ/∫ρ\rho_{\mathrm{n}}=\rho/\int\rho be its normalization. Then for all z,v∈Cz,v\in\mathbb{C}, D(ρn∗φ)(z) v=(ρn∗(Dφ(⋅) v))(z)D(\rho_{\mathrm{n}}*\varphi)(z)\,v=\big(\rho_{\mathrm{n}}*(D\varphi(\cdot)\,v)\big)(z).

Formalization Note For a bump function ρ\rho centred at 00 (ContDiffBump (0 : ℂ)), ρn\rho_{\mathrm{n}} is ρ.normed volume, the multiple of ρ\rho with integral 11; ρn∗g\rho_{\mathrm{n}}*g is the convolution ρ.normed volume ⋆[lsmul ℝ ℝ, volume] g with respect to Lebesgue measure on C\mathbb{C}. The derivatives are fderiv ℝ.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Calculus.ContDiff.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Formal statement
namespace JHolomorphic

open MeasureTheory Filter Topology Metric ContinuousLinearMap
open scoped ContDiff Convolution

/-- Directional derivatives of a mollified `C¹` function are mollified directional derivatives. -/
theorem fderiv_normed_convolution_apply (ρ : ContDiffBump (0 : ℂ)) (φ : ℂ → ℝ)
    (hφ : ContDiff ℝ 1 φ) (hc : HasCompactSupport φ) (z v : ℂ) :
    fderiv ℝ (ρ.normed volume ⋆[lsmul ℝ ℝ, volume] φ) z v =
      (ρ.normed volume ⋆[lsmul ℝ ℝ, volume] fun x => fderiv ℝ φ x v) z := by
  sorry

end JHolomorphic
Source
Standard (mollification).

View graph