A function $C^n$ on $U$ times a $C^n$ function supported in $U$ is $C^n$ on $\mathbb{C}$

Proved

JHolomorphic.contDiff_mul_of_tsupport_subset

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

sobolev-spacesweak-derivatives

Let $U\subseteq\mathbb{C}$ be open, $n\in\mathbb{N}\cup\{\infty\}$ , let $\varphi:\mathbb{C}\to\mathbb{R}$ be $C^n$ with closed support contained in $U$ , and let $a:\mathbb{C}\to\mathbb{R}$ be $C^n$ on $U$ . Then $z\mapsto\varphi(z)\,a(z)$ is $C^n$ on all of $\mathbb{C}$ .

Formalization Note $n$ is an ℕ∞; the hypotheses are ContDiff ℝ n φ, tsupport φ ⊆ U, ContDiffOn ℝ n a 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

/-- The product of a `Cⁿ` function with closed support in an open set `U` and a function that
is `Cⁿ` on `U` is `Cⁿ` on all of `ℂ`. -/
theorem contDiff_mul_of_tsupport_subset {U : Set ℂ} (hU : IsOpen U) {n : ℕ∞} {φ a : ℂ → ℝ}
    (hφ : ContDiff ℝ n φ) (hφU : tsupport φ ⊆ U) (ha : ContDiffOn ℝ n a U) :
    ContDiff ℝ n (fun z => φ z * a z) := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and distribution theory).

View graph

A function CnC^nCn on UUU times a CnC^nCn function supported in UUU is CnC^nCn on C\mathbb{C}C

A function $C^n$ on $U$ times a $C^n$ function supported in $U$ is $C^n$ on $\mathbb{C}$