Directional derivatives of test functions on $U\subseteq\mathbb{C}$ are test functions on $U$

Proved

JHolomorphic.fderiv_apply_isTestFunction

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

sobolev-spacesweak-derivatives

Let $\varphi:\mathbb{C}\to\mathbb{R}$ be $C^\infty$ with compact support contained in $U\subseteq\mathbb{C}$ , and let $v\in\mathbb{C}$ . Then $z\mapsto D\varphi(z)\,v$ is again $C^\infty$ with compact support contained in $U$ .

Formalization Note $D\varphi(z)\,v$ is fderiv ℝ φ z v; the support conditions are HasCompactSupport and tsupport · ⊆ U.

Preamble

import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp

Formal statement

namespace JHolomorphic

open MeasureTheory Filter Topology
open scoped ContDiff

/-- A directional derivative `z ↦ Dφ(z) v` of a real `C^∞` function `φ` with compact support in
`U` is again a real `C^∞` function with compact support in `U`. -/
theorem fderiv_apply_isTestFunction {U : Set ℂ} {φ : ℂ → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ U) (v : ℂ) :
    ContDiff ℝ ∞ (fun z => fderiv ℝ φ z v) ∧ HasCompactSupport (fun z => fderiv ℝ φ z v) ∧
      tsupport (fun z => fderiv ℝ φ z v) ⊆ U := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and distribution theory).

View graph

Directional derivatives of test functions on U⊆CU\subseteq\mathbb{C}U⊆C are test functions on UUU

Directional derivatives of test functions on $U\subseteq\mathbb{C}$ are test functions on $U$