Support and singular support rules for convolution (source code)

= Support and singular support rules for convolution

If at least one of $u,v\in\mathcal D'(\mathbb R^n)$ is a <compactly supported distribution>, then
$$
\operatorname{supp}(u*v)\subseteq\operatorname{supp}u+\operatorname{supp}v,\qquad
\operatorname{sing\,supp}(u*v)\subseteq\operatorname{sing\,supp}u+\operatorname{sing\,supp}v.
$$
The sums are <Minkowski sums>. The first rule follows from the pairing $\langle u_x\otimes v_y,\phi(x+y)\rangle$: a <test function> away from the support sum gives zero. For the second rule, localize the output to a small <compact set> avoiding the sum of the <singular supports>. The relevant pairs of input points form a <compact set> because one input <support> is compact. Cover it by finitely many product neighborhoods on each of which at least one input <distribution> is smooth; otherwise the output would meet the sum of the <singular supports>. Smooth cutoffs in these neighborhoods decompose the localized pairing into finitely many <convolutions> with a smooth compactly supported factor. Each is smooth by <smoothing convolution with a test function>. This proves the second rule locally.

The same argument works when addition is a <proper map> on the product of the two <supports>. Some condition defining the <convolution> is necessary; arbitrary pairs of <distributions> cannot always be convolved.

``
Target: Cauchy kernel fundamental solution. Parent: Fundamental solution of a linear differential operator. Intended file: distribution-theory.bigb.
``