Iterated derivatives of Schwartz convolution

Every finite ordered spatial derivative may be transferred from the convolution to its scalar Schwartz kernel.

theorem CKN.Leray.regularised_schwartz_convolution_iteratedLineDeriv (κ : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (n : ℕ) (m : Fin n → Foundation.Parabolic.L2Vec3) : LineDeriv.iteratedLineDerivOp m (((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) κ) ψ) = ((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) (LineDeriv.iteratedLineDerivOp m κ)) ψ

All finite ordered line derivatives commute with convolution by a scalar Schwartz kernel.