Derivatives of Schwartz convolution

Spatial differentiation may be moved from a convolution onto its Schwartz kernel.

theorem CKN.Leray.regularised_schwartz_convolution_lineDeriv (κ : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (m : Foundation.Parabolic.L2Vec3) : LineDeriv.lineDerivOp m (((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) κ) ψ) = ((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) (LineDeriv.lineDerivOp m κ)) ψ

A line derivative of scalar-kernel/vector-field Schwartz convolution equals convolution with the corresponding derivative of the kernel.